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

Metamath Proof Explorer

Theorem opeliunxp2

Description: Membership in a union of Cartesian products. (Contributed by Mario Carneiro, 14-Feb-2015)

Ref Expression
Hypothesis opeliunxp2.1 
|- ( x = C -> B = E )
Assertion opeliunxp2 
|- ( <. C , D >. e. U_ x e. A ( { x } X. B ) <-> ( C e. A /\ D e. E ) )

Proof

Step Hyp Ref Expression
1 opeliunxp2.1 
 |-  ( x = C -> B = E )
2 df-br 
 |-  ( C U_ x e. A ( { x } X. B ) D <-> <. C , D >. e. U_ x e. A ( { x } X. B ) )
3 relxp 
 |-  Rel ( { x } X. B )
4 3 rgenw 
 |-  A. x e. A Rel ( { x } X. B )
5 reliun 
 |-  ( Rel U_ x e. A ( { x } X. B ) <-> A. x e. A Rel ( { x } X. B ) )
6 4 5 mpbir 
 |-  Rel U_ x e. A ( { x } X. B )
7 6 brrelex1i 
 |-  ( C U_ x e. A ( { x } X. B ) D -> C e. _V )
8 2 7 sylbir 
 |-  ( <. C , D >. e. U_ x e. A ( { x } X. B ) -> C e. _V )
9 elex 
 |-  ( C e. A -> C e. _V )
10 9 adantr 
 |-  ( ( C e. A /\ D e. E ) -> C e. _V )
11 nfiu1 
 |-  F/_ x U_ x e. A ( { x } X. B )
12 11 nfel2 
 |-  F/ x <. C , D >. e. U_ x e. A ( { x } X. B )
13 nfv 
 |-  F/ x ( C e. A /\ D e. E )
14 12 13 nfbi 
 |-  F/ x ( <. C , D >. e. U_ x e. A ( { x } X. B ) <-> ( C e. A /\ D e. E ) )
15 opeq1 
 |-  ( x = C -> <. x , D >. = <. C , D >. )
16 15 eleq1d 
 |-  ( x = C -> ( <. x , D >. e. U_ x e. A ( { x } X. B ) <-> <. C , D >. e. U_ x e. A ( { x } X. B ) ) )
17 eleq1 
 |-  ( x = C -> ( x e. A <-> C e. A ) )
18 1 eleq2d 
 |-  ( x = C -> ( D e. B <-> D e. E ) )
19 17 18 anbi12d 
 |-  ( x = C -> ( ( x e. A /\ D e. B ) <-> ( C e. A /\ D e. E ) ) )
20 16 19 bibi12d 
 |-  ( x = C -> ( ( <. x , D >. e. U_ x e. A ( { x } X. B ) <-> ( x e. A /\ D e. B ) ) <-> ( <. C , D >. e. U_ x e. A ( { x } X. B ) <-> ( C e. A /\ D e. E ) ) ) )
21 opeliunxp 
 |-  ( <. x , D >. e. U_ x e. A ( { x } X. B ) <-> ( x e. A /\ D e. B ) )
22 14 20 21 vtoclg1f 
 |-  ( C e. _V -> ( <. C , D >. e. U_ x e. A ( { x } X. B ) <-> ( C e. A /\ D e. E ) ) )
23 8 10 22 pm5.21nii 
 |-  ( <. C , D >. e. U_ x e. A ( { x } X. B ) <-> ( C e. A /\ D e. E ) )