Description: Version of 19.42 with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 21Jun1993)
Ref  Expression  

Assertion  19.42v   ( E. x ( ph /\ ps ) <> ( ph /\ E. x ps ) ) 
Step  Hyp  Ref  Expression 

1  19.41v   ( E. x ( ps /\ ph ) <> ( E. x ps /\ ph ) ) 

2  exancom   ( E. x ( ph /\ ps ) <> E. x ( ps /\ ph ) ) 

3  ancom   ( ( ph /\ E. x ps ) <> ( E. x ps /\ ph ) ) 

4  1 2 3  3bitr4i   ( E. x ( ph /\ ps ) <> ( ph /\ E. x ps ) ) 