Metamath Proof Explorer

Theorem r19.45zv

Description: Restricted version of Theorem 19.45 of Margaris p. 90. (Contributed by NM, 27-May-1998)

Ref Expression
Assertion r19.45zv 
|- ( A =/= (/) -> ( E. x e. A ( ph \/ ps ) <-> ( ph \/ E. x e. A ps ) ) )

Proof

Step Hyp Ref Expression
1 r19.43 
 |-  ( E. x e. A ( ph \/ ps ) <-> ( E. x e. A ph \/ E. x e. A ps ) )
2 r19.9rzv 
 |-  ( A =/= (/) -> ( ph <-> E. x e. A ph ) )
3 2 orbi1d 
 |-  ( A =/= (/) -> ( ( ph \/ E. x e. A ps ) <-> ( E. x e. A ph \/ E. x e. A ps ) ) )
4 1 3 bitr4id 
 |-  ( A =/= (/) -> ( E. x e. A ( ph \/ ps ) <-> ( ph \/ E. x e. A ps ) ) )