Metamath Proof Explorer

Theorem ralunb

Description: Restricted quantification over a union. (Contributed by Scott Fenton, 12-Apr-2011) (Proof shortened by Andrew Salmon, 29-Jun-2011)

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

Proof

Step Hyp Ref Expression
1 elunant 
 |-  ( ( x e. ( A u. B ) -> ph ) <-> ( ( x e. A -> ph ) /\ ( x e. B -> ph ) ) )
2 1 albii 
 |-  ( A. x ( x e. ( A u. B ) -> ph ) <-> A. x ( ( x e. A -> ph ) /\ ( x e. B -> ph ) ) )
3 19.26 
 |-  ( A. x ( ( x e. A -> ph ) /\ ( x e. B -> ph ) ) <-> ( A. x ( x e. A -> ph ) /\ A. x ( x e. B -> ph ) ) )
4 2 3 bitri 
 |-  ( A. x ( x e. ( A u. B ) -> ph ) <-> ( A. x ( x e. A -> ph ) /\ A. x ( x e. B -> ph ) ) )
5 df-ral 
 |-  ( A. x e. ( A u. B ) ph <-> A. x ( x e. ( A u. B ) -> ph ) )
6 df-ral 
 |-  ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
7 df-ral 
 |-  ( A. x e. B ph <-> A. x ( x e. B -> ph ) )
8 6 7 anbi12i 
 |-  ( ( A. x e. A ph /\ A. x e. B ph ) <-> ( A. x ( x e. A -> ph ) /\ A. x ( x e. B -> ph ) ) )
9 4 5 8 3bitr4i 
 |-  ( A. x e. ( A u. B ) ph <-> ( A. x e. A ph /\ A. x e. B ph ) )