Metamath Proof Explorer

Theorem eliunxp

Description: Membership in a union of Cartesian products. Analogue of elxp for nonconstant B ( x ) . (Contributed by Mario Carneiro, 29-Dec-2014)

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

Proof

Step Hyp Ref Expression
1 relxp 
 |-  Rel ( { x } X. B )
2 1 rgenw 
 |-  A. x e. A Rel ( { x } X. B )
3 reliun 
 |-  ( Rel U_ x e. A ( { x } X. B ) <-> A. x e. A Rel ( { x } X. B ) )
4 2 3 mpbir 
 |-  Rel U_ x e. A ( { x } X. B )
5 elrel 
 |-  ( ( Rel U_ x e. A ( { x } X. B ) /\ C e. U_ x e. A ( { x } X. B ) ) -> E. x E. y C = <. x , y >. )
6 4 5 mpan 
 |-  ( C e. U_ x e. A ( { x } X. B ) -> E. x E. y C = <. x , y >. )
7 6 pm4.71ri 
 |-  ( C e. U_ x e. A ( { x } X. B ) <-> ( E. x E. y C = <. x , y >. /\ C e. U_ x e. A ( { x } X. B ) ) )
8 nfiu1 
 |-  F/_ x U_ x e. A ( { x } X. B )
9 8 nfel2 
 |-  F/ x C e. U_ x e. A ( { x } X. B )
10 9 19.41 
 |-  ( E. x ( E. y C = <. x , y >. /\ C e. U_ x e. A ( { x } X. B ) ) <-> ( E. x E. y C = <. x , y >. /\ C e. U_ x e. A ( { x } X. B ) ) )
11 19.41v 
 |-  ( E. y ( C = <. x , y >. /\ C e. U_ x e. A ( { x } X. B ) ) <-> ( E. y C = <. x , y >. /\ C e. U_ x e. A ( { x } X. B ) ) )
12 eleq1 
 |-  ( C = <. x , y >. -> ( C e. U_ x e. A ( { x } X. B ) <-> <. x , y >. e. U_ x e. A ( { x } X. B ) ) )
13 opeliunxp 
 |-  ( <. x , y >. e. U_ x e. A ( { x } X. B ) <-> ( x e. A /\ y e. B ) )
14 12 13 bitrdi 
 |-  ( C = <. x , y >. -> ( C e. U_ x e. A ( { x } X. B ) <-> ( x e. A /\ y e. B ) ) )
15 14 pm5.32i 
 |-  ( ( C = <. x , y >. /\ C e. U_ x e. A ( { x } X. B ) ) <-> ( C = <. x , y >. /\ ( x e. A /\ y e. B ) ) )
16 15 exbii 
 |-  ( E. y ( C = <. x , y >. /\ C e. U_ x e. A ( { x } X. B ) ) <-> E. y ( C = <. x , y >. /\ ( x e. A /\ y e. B ) ) )
17 11 16 bitr3i 
 |-  ( ( E. y C = <. x , y >. /\ C e. U_ x e. A ( { x } X. B ) ) <-> E. y ( C = <. x , y >. /\ ( x e. A /\ y e. B ) ) )
18 17 exbii 
 |-  ( E. x ( E. y C = <. x , y >. /\ C e. U_ x e. A ( { x } X. B ) ) <-> E. x E. y ( C = <. x , y >. /\ ( x e. A /\ y e. B ) ) )
19 7 10 18 3bitr2i 
 |-  ( C e. U_ x e. A ( { x } X. B ) <-> E. x E. y ( C = <. x , y >. /\ ( x e. A /\ y e. B ) ) )