Metamath Proof Explorer

Theorem r19.30

Description: Restricted quantifier version of 19.30 . (Contributed by Scott Fenton, 25-Feb-2011) (Proof shortened by Wolf Lammen, 5-Nov-2024)

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

Proof

Step Hyp Ref Expression
1 pm2.53 
 |-  ( ( ph \/ ps ) -> ( -. ph -> ps ) )
2 1 ralimi 
 |-  ( A. x e. A ( ph \/ ps ) -> A. x e. A ( -. ph -> ps ) )
3 rexnal 
 |-  ( E. x e. A -. ph <-> -. A. x e. A ph )
4 3 biimpri 
 |-  ( -. A. x e. A ph -> E. x e. A -. ph )
5 rexim 
 |-  ( A. x e. A ( -. ph -> ps ) -> ( E. x e. A -. ph -> E. x e. A ps ) )
6 2 4 5 syl2im 
 |-  ( A. x e. A ( ph \/ ps ) -> ( -. A. x e. A ph -> E. x e. A ps ) )
7 6 orrd 
 |-  ( A. x e. A ( ph \/ ps ) -> ( A. x e. A ph \/ E. x e. A ps ) )