Metamath Proof Explorer


Theorem r19.44zv

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

Ref Expression
Assertion r19.44zv
|- ( A =/= (/) -> ( E. x e. A ( ph \/ ps ) <-> ( E. x e. A ph \/ 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 =/= (/) -> ( ps <-> E. x e. A ps ) )
3 2 orbi2d
 |-  ( A =/= (/) -> ( ( E. x e. A ph \/ ps ) <-> ( E. x e. A ph \/ E. x e. A ps ) ) )
4 1 3 bitr4id
 |-  ( A =/= (/) -> ( E. x e. A ( ph \/ ps ) <-> ( E. x e. A ph \/ ps ) ) )