This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem r19.42v

Description: Restricted quantifier version of 19.42v (see also 19.42 ). (Contributed by NM, 27-May-1998)

Ref Expression
Assertion r19.42v 
|- ( E. x e. A ( ph /\ ps ) <-> ( ph /\ E. x e. A ps ) )

Proof

Step Hyp Ref Expression
1 r19.41v 
 |-  ( E. x e. A ( ps /\ ph ) <-> ( E. x e. A ps /\ ph ) )
2 ancom 
 |-  ( ( ph /\ ps ) <-> ( ps /\ ph ) )
3 2 rexbii 
 |-  ( E. x e. A ( ph /\ ps ) <-> E. x e. A ( ps /\ ph ) )
4 ancom 
 |-  ( ( ph /\ E. x e. A ps ) <-> ( E. x e. A ps /\ ph ) )
5 1 3 4 3bitr4i 
 |-  ( E. x e. A ( ph /\ ps ) <-> ( ph /\ E. x e. A ps ) )