Metamath Proof Explorer

Theorem r19.43

Description: Restricted quantifier version of 19.43 . (Contributed by NM, 27-May-1998) (Proof shortened by Andrew Salmon, 30-May-2011)

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

Proof

Step Hyp Ref Expression
1 r19.35 
 |-  ( E. x e. A ( -. ph -> ps ) <-> ( A. x e. A -. ph -> E. x e. A ps ) )
2 df-or 
 |-  ( ( ph \/ ps ) <-> ( -. ph -> ps ) )
3 2 rexbii 
 |-  ( E. x e. A ( ph \/ ps ) <-> E. x e. A ( -. ph -> ps ) )
4 df-or 
 |-  ( ( E. x e. A ph \/ E. x e. A ps ) <-> ( -. E. x e. A ph -> E. x e. A ps ) )
5 ralnex 
 |-  ( A. x e. A -. ph <-> -. E. x e. A ph )
6 5 imbi1i 
 |-  ( ( A. x e. A -. ph -> E. x e. A ps ) <-> ( -. E. x e. A ph -> E. x e. A ps ) )
7 4 6 bitr4i 
 |-  ( ( E. x e. A ph \/ E. x e. A ps ) <-> ( A. x e. A -. ph -> E. x e. A ps ) )
8 1 3 7 3bitr4i 
 |-  ( E. x e. A ( ph \/ ps ) <-> ( E. x e. A ph \/ E. x e. A ps ) )