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

Metamath Proof Explorer

Theorem 2ralor

Description: Distribute restricted universal quantification over "or". (Contributed by Jeff Madsen, 19-Jun-2010) Shorten, reduce dv conditions. (Revised by Wolf Lammen, 20-Nov-2024)

Ref Expression
Assertion 2ralor 
|- ( A. x e. A A. y e. B ( ph \/ ps ) <-> ( A. x e. A ph \/ A. y e. B ps ) )

Proof

Step Hyp Ref Expression
1 r19.32v 
 |-  ( A. y e. B ( ph \/ ps ) <-> ( ph \/ A. y e. B ps ) )
2 orcom 
 |-  ( ( ph \/ A. y e. B ps ) <-> ( A. y e. B ps \/ ph ) )
3 1 2 bitri 
 |-  ( A. y e. B ( ph \/ ps ) <-> ( A. y e. B ps \/ ph ) )
4 3 ralbii 
 |-  ( A. x e. A A. y e. B ( ph \/ ps ) <-> A. x e. A ( A. y e. B ps \/ ph ) )
5 r19.32v 
 |-  ( A. x e. A ( A. y e. B ps \/ ph ) <-> ( A. y e. B ps \/ A. x e. A ph ) )
6 orcom 
 |-  ( ( A. y e. B ps \/ A. x e. A ph ) <-> ( A. x e. A ph \/ A. y e. B ps ) )
7 4 5 6 3bitri 
 |-  ( A. x e. A A. y e. B ( ph \/ ps ) <-> ( A. x e. A ph \/ A. y e. B ps ) )