Theorem opeliunxp

Description: Membership in a union of Cartesian products. (Contributed by Mario Carneiro, 29-Dec-2014) (Revised by Mario Carneiro, 1-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		df-iun	|- U_ x e. A ( { x } X. B ) = { y | E. x e. A y e. ( { x } X. B ) }
2	1	eleq2i	|- ( <. x , C >. e. U_ x e. A ( { x } X. B ) <-> <. x , C >. e. { y | E. x e. A y e. ( { x } X. B ) } )
3		opex	|- <. x , C >. e. _V
4		df-rex	|- ( E. x e. A y e. ( { x } X. B ) <-> E. x ( x e. A /\ y e. ( { x } X. B ) ) )
5		nfv	|- F/ z ( x e. A /\ y e. ( { x } X. B ) )
6		nfs1v	|- F/ x [ z / x ] x e. A
7		nfcv	|- F/_ x { z }
8		nfcsb1v	|- F/_ x [_ z / x ]_ B
9	7 8	nfxp	|- F/_ x ( { z } X. [_ z / x ]_ B )
10	9	nfcri	|- F/ x y e. ( { z } X. [_ z / x ]_ B )
11	6 10	nfan	|- F/ x ( [ z / x ] x e. A /\ y e. ( { z } X. [_ z / x ]_ B ) )
12		sbequ12	|- ( x = z -> ( x e. A <-> [ z / x ] x e. A ) )
13		sneq	|- ( x = z -> { x } = { z } )
14		csbeq1a	|- ( x = z -> B = [_ z / x ]_ B )
15	13 14	xpeq12d	|- ( x = z -> ( { x } X. B ) = ( { z } X. [_ z / x ]_ B ) )
16	15	eleq2d	|- ( x = z -> ( y e. ( { x } X. B ) <-> y e. ( { z } X. [_ z / x ]_ B ) ) )
17	12 16	anbi12d	|- ( x = z -> ( ( x e. A /\ y e. ( { x } X. B ) ) <-> ( [ z / x ] x e. A /\ y e. ( { z } X. [_ z / x ]_ B ) ) ) )
18	5 11 17	cbvexv1	|- ( E. x ( x e. A /\ y e. ( { x } X. B ) ) <-> E. z ( [ z / x ] x e. A /\ y e. ( { z } X. [_ z / x ]_ B ) ) )
19	4 18	bitri	|- ( E. x e. A y e. ( { x } X. B ) <-> E. z ( [ z / x ] x e. A /\ y e. ( { z } X. [_ z / x ]_ B ) ) )
20		eleq1	|- ( y = <. x , C >. -> ( y e. ( { z } X. [_ z / x ]_ B ) <-> <. x , C >. e. ( { z } X. [_ z / x ]_ B ) ) )
21	20	anbi2d	|- ( y = <. x , C >. -> ( ( [ z / x ] x e. A /\ y e. ( { z } X. [_ z / x ]_ B ) ) <-> ( [ z / x ] x e. A /\ <. x , C >. e. ( { z } X. [_ z / x ]_ B ) ) ) )
22	21	exbidv	|- ( y = <. x , C >. -> ( E. z ( [ z / x ] x e. A /\ y e. ( { z } X. [_ z / x ]_ B ) ) <-> E. z ( [ z / x ] x e. A /\ <. x , C >. e. ( { z } X. [_ z / x ]_ B ) ) ) )
23	19 22	bitrid	|- ( y = <. x , C >. -> ( E. x e. A y e. ( { x } X. B ) <-> E. z ( [ z / x ] x e. A /\ <. x , C >. e. ( { z } X. [_ z / x ]_ B ) ) ) )
24	3 23	elab	|- ( <. x , C >. e. { y | E. x e. A y e. ( { x } X. B ) } <-> E. z ( [ z / x ] x e. A /\ <. x , C >. e. ( { z } X. [_ z / x ]_ B ) ) )
25		opelxp	|- ( <. x , C >. e. ( { z } X. [_ z / x ]_ B ) <-> ( x e. { z } /\ C e. [_ z / x ]_ B ) )
26	25	anbi2i	|- ( ( [ z / x ] x e. A /\ <. x , C >. e. ( { z } X. [_ z / x ]_ B ) ) <-> ( [ z / x ] x e. A /\ ( x e. { z } /\ C e. [_ z / x ]_ B ) ) )
27		an12	|- ( ( [ z / x ] x e. A /\ ( x e. { z } /\ C e. [_ z / x ]_ B ) ) <-> ( x e. { z } /\ ( [ z / x ] x e. A /\ C e. [_ z / x ]_ B ) ) )
28		velsn	|- ( x e. { z } <-> x = z )
29		equcom	|- ( x = z <-> z = x )
30	28 29	bitri	|- ( x e. { z } <-> z = x )
31	30	anbi1i	|- ( ( x e. { z } /\ ( [ z / x ] x e. A /\ C e. [_ z / x ]_ B ) ) <-> ( z = x /\ ( [ z / x ] x e. A /\ C e. [_ z / x ]_ B ) ) )
32	26 27 31	3bitri	|- ( ( [ z / x ] x e. A /\ <. x , C >. e. ( { z } X. [_ z / x ]_ B ) ) <-> ( z = x /\ ( [ z / x ] x e. A /\ C e. [_ z / x ]_ B ) ) )
33	32	exbii	|- ( E. z ( [ z / x ] x e. A /\ <. x , C >. e. ( { z } X. [_ z / x ]_ B ) ) <-> E. z ( z = x /\ ( [ z / x ] x e. A /\ C e. [_ z / x ]_ B ) ) )
34		sbequ12r	|- ( z = x -> ( [ z / x ] x e. A <-> x e. A ) )
35	14	equcoms	|- ( z = x -> B = [_ z / x ]_ B )
36	35	eqcomd	|- ( z = x -> [_ z / x ]_ B = B )
37	36	eleq2d	|- ( z = x -> ( C e. [_ z / x ]_ B <-> C e. B ) )
38	34 37	anbi12d	|- ( z = x -> ( ( [ z / x ] x e. A /\ C e. [_ z / x ]_ B ) <-> ( x e. A /\ C e. B ) ) )
39	38	equsexvw	|- ( E. z ( z = x /\ ( [ z / x ] x e. A /\ C e. [_ z / x ]_ B ) ) <-> ( x e. A /\ C e. B ) )
40	33 39	bitri	|- ( E. z ( [ z / x ] x e. A /\ <. x , C >. e. ( { z } X. [_ z / x ]_ B ) ) <-> ( x e. A /\ C e. B ) )
41	2 24 40	3bitri	|- ( <. x , C >. e. U_ x e. A ( { x } X. B ) <-> ( x e. A /\ C e. B ) )