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

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 ) ) )