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

Metamath Proof Explorer

Theorem r19.32v

Description: Restricted quantifier version of 19.32v . (Contributed by NM, 25-Nov-2003)

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

Proof

Step Hyp Ref Expression
1 r19.21v 
 |-  ( A. x e. A ( -. ph -> ps ) <-> ( -. ph -> A. x e. A ps ) )
2 df-or 
 |-  ( ( ph \/ ps ) <-> ( -. ph -> ps ) )
3 2 ralbii 
 |-  ( A. x e. A ( ph \/ ps ) <-> A. x e. A ( -. ph -> ps ) )
4 df-or 
 |-  ( ( ph \/ A. x e. A ps ) <-> ( -. ph -> A. x e. A ps ) )
5 1 3 4 3bitr4i 
 |-  ( A. x e. A ( ph \/ ps ) <-> ( ph \/ A. x e. A ps ) )