let p, q be ZF-formula; :: thesis: for M being non empty set st M |= p => q & M |= p holds
M |= q
let M be non empty set ; :: thesis: ( M |= p => q & M |= p implies M |= q )
assume A1: ( M |= p => q & M |= p ) ; :: thesis: M |= q
let v be Function of VAR,M; :: according to ZF_MODEL:def 5 :: thesis: M,v |= q
( M,v |= p => q & M,v |= p ) by A1;
hence M,v |= q by ZF_MODEL:18; :: thesis: verum