let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st p <==> q holds
Ex (x,p) <==> Ex (x,q)
let p, q be Element of CQC-WFF A; :: thesis: for x being bound_QC-variable of A st p <==> q holds
Ex (x,p) <==> Ex (x,q)
let x be bound_QC-variable of A; :: thesis: ( p <==> q implies Ex (x,p) <==> Ex (x,q) )
assume p <==> q ; :: thesis: Ex (x,p) <==> Ex (x,q)
then 'not' p <==> 'not' q by Lm5;
then All (x,('not' p)) <==> All (x,('not' q)) by Th58;
then A1: 'not' (All (x,('not' p))) <==> 'not' (All (x,('not' q))) by Lm5;
Ex (x,p) = 'not' (All (x,('not' p))) by QC_LANG2:def 5;
hence Ex (x,p) <==> Ex (x,q) by A1, QC_LANG2:def 5; :: thesis: verum