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

Metamath Proof Explorer

Theorem rexun

Description: Restricted existential quantification over union. (Contributed by Jeff Madsen, 5-Jan-2011)

Ref Expression
Assertion rexun 
|- ( E. x e. ( A u. B ) ph <-> ( E. x e. A ph \/ E. x e. B ph ) )

Proof

Step Hyp Ref Expression
1 df-rex 
 |-  ( E. x e. ( A u. B ) ph <-> E. x ( x e. ( A u. B ) /\ ph ) )
2 19.43 
 |-  ( E. x ( ( x e. A /\ ph ) \/ ( x e. B /\ ph ) ) <-> ( E. x ( x e. A /\ ph ) \/ E. x ( x e. B /\ ph ) ) )
3 elun 
 |-  ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
4 3 anbi1i 
 |-  ( ( x e. ( A u. B ) /\ ph ) <-> ( ( x e. A \/ x e. B ) /\ ph ) )
5 andir 
 |-  ( ( ( x e. A \/ x e. B ) /\ ph ) <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ ph ) ) )
6 4 5 bitri 
 |-  ( ( x e. ( A u. B ) /\ ph ) <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ ph ) ) )
7 6 exbii 
 |-  ( E. x ( x e. ( A u. B ) /\ ph ) <-> E. x ( ( x e. A /\ ph ) \/ ( x e. B /\ ph ) ) )
8 df-rex 
 |-  ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
9 df-rex 
 |-  ( E. x e. B ph <-> E. x ( x e. B /\ ph ) )
10 8 9 orbi12i 
 |-  ( ( E. x e. A ph \/ E. x e. B ph ) <-> ( E. x ( x e. A /\ ph ) \/ E. x ( x e. B /\ ph ) ) )
11 2 7 10 3bitr4i 
 |-  ( E. x ( x e. ( A u. B ) /\ ph ) <-> ( E. x e. A ph \/ E. x e. B ph ) )
12 1 11 bitri 
 |-  ( E. x e. ( A u. B ) ph <-> ( E. x e. A ph \/ E. x e. B ph ) )