Theorem opeliunxp 4395

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

Assertion

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

Proof of Theorem opeliunxp

Dummy variables y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 2566	. 2 |- ( <. x , C >. e. U_ x e. A ( { x } X. B ) -> <. x , C >. e. _V )
2		vex 2560	. . 3 |- x e. _V
3		elex 2566	. . . 4 |- ( C e. B -> C e. _V )
4	3	adantl 262	. . 3 |- ( ( x e. A /\ C e. B ) -> C e. _V )
5		opexgOLD 3965	. . 3 |- ( ( x e. _V /\ C e. _V ) -> <. x , C >. e. _V )
6	2, 4, 5	sylancr 393	. 2 |- ( ( x e. A /\ C e. B ) -> <. x , C >. e. _V )
7		df-rex 2312	. . . . . 6 |- ( E. x e. A y e. ( { x } X. B ) <-> E. x ( x e. A /\ y e. ( { x } X. B ) ) )
8		nfv 1421	. . . . . . 7 |- F/ z ( x e. A /\ y e. ( { x } X. B ) )
9		nfs1v 1815	. . . . . . . 8 |- F/ x [ z / x ] x e. A
10		nfcv 2178	. . . . . . . . . 10 |- F/_ x { z }
11		nfcsb1v 2882	. . . . . . . . . 10 |- F/_ x [_ z / x ]_ B
12	10, 11	nfxp 4371	. . . . . . . . 9 |- F/_ x ( { z } X. [_ z / x ]_ B )
13	12	nfcri 2172	. . . . . . . 8 |- F/ x y e. ( { z } X. [_ z / x ]_ B )
14	9, 13	nfan 1457	. . . . . . 7 |- F/ x ( [ z / x ] x e. A /\ y e. ( { z } X. [_ z / x ]_ B ) )
15		sbequ12 1654	. . . . . . . 8 |- ( x = z -> ( x e. A <-> [ z / x ] x e. A ) )
16		sneq 3386	. . . . . . . . . 10 |- ( x = z -> { x } = { z } )
17		csbeq1a 2860	. . . . . . . . . 10 |- ( x = z -> B = [_ z / x ]_ B )
18	16, 17	xpeq12d 4370	. . . . . . . . 9 |- ( x = z -> ( { x } X. B ) = ( { z } X. [_ z / x ]_ B ) )
19	18	eleq2d 2107	. . . . . . . 8 |- ( x = z -> ( y e. ( { x } X. B ) <-> y e. ( { z } X. [_ z / x ]_ B ) ) )
20	15, 19	anbi12d 442	. . . . . . 7 |- ( x = z -> ( ( x e. A /\ y e. ( { x } X. B ) ) <-> ( [ z / x ] x e. A /\ y e. ( { z } X. [_ z / x ]_ B ) ) ) )
21	8, 14, 20	cbvex 1639	. . . . . 6 |- ( E. x ( x e. A /\ y e. ( { x } X. B ) ) <-> E. z ( [ z / x ] x e. A /\ y e. ( { z } X. [_ z / x ]_ B ) ) )
22	7, 21	bitri 173	. . . . 5 |- ( E. x e. A y e. ( { x } X. B ) <-> E. z ( [ z / x ] x e. A /\ y e. ( { z } X. [_ z / x ]_ B ) ) )
23		eleq1 2100	. . . . . . 7 |- ( y = <. x , C >. -> ( y e. ( { z } X. [_ z / x ]_ B ) <-> <. x , C >. e. ( { z } X. [_ z / x ]_ B ) ) )
24	23	anbi2d 437	. . . . . 6 |- ( 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 ) ) ) )
25	24	exbidv 1706	. . . . 5 |- ( 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 ) ) ) )
26	22, 25	syl5bb 181	. . . 4 |- ( 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 ) ) ) )
27		df-iun 3659	. . . 4 |- U_ x e. A ( { x } X. B ) = { y | E. x e. A y e. ( { x } X. B ) }
28	26, 27	elab2g 2689	. . 3 |- ( <. x , C >. e. _V -> ( <. x , C >. e. U_ x e. A ( { x } X. B ) <-> E. z ( [ z / x ] x e. A /\ <. x , C >. e. ( { z } X. [_ z / x ]_ B ) ) ) )
29		opelxp 4374	. . . . . . 7 |- ( <. x , C >. e. ( { z } X. [_ z / x ]_ B ) <-> ( x e. { z } /\ C e. [_ z / x ]_ B ) )
30	29	anbi2i 430	. . . . . 6 |- ( ( [ 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 ) ) )
31		an12 495	. . . . . 6 |- ( ( [ 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 ) ) )
32		velsn 3392	. . . . . . . 8 |- ( x e. { z } <-> x = z )
33		equcom 1593	. . . . . . . 8 |- ( x = z <-> z = x )
34	32, 33	bitri 173	. . . . . . 7 |- ( x e. { z } <-> z = x )
35	34	anbi1i 431	. . . . . 6 |- ( ( 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 ) ) )
36	30, 31, 35	3bitri 195	. . . . 5 |- ( ( [ 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 ) ) )
37	36	exbii 1496	. . . 4 |- ( 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 ) ) )
38		sbequ12r 1655	. . . . . 6 |- ( z = x -> ( [ z / x ] x e. A <-> x e. A ) )
39	17	equcoms 1594	. . . . . . . 8 |- ( z = x -> B = [_ z / x ]_ B )
40	39	eqcomd 2045	. . . . . . 7 |- ( z = x -> [_ z / x ]_ B = B )
41	40	eleq2d 2107	. . . . . 6 |- ( z = x -> ( C e. [_ z / x ]_ B <-> C e. B ) )
42	38, 41	anbi12d 442	. . . . 5 |- ( z = x -> ( ( [ z / x ] x e. A /\ C e. [_ z / x ]_ B ) <-> ( x e. A /\ C e. B ) ) )
43	2, 42	ceqsexv 2593	. . . 4 |- ( E. z ( z = x /\ ( [ z / x ] x e. A /\ C e. [_ z / x ]_ B ) ) <-> ( x e. A /\ C e. B ) )
44	37, 43	bitri 173	. . 3 |- ( E. z ( [ z / x ] x e. A /\ <. x , C >. e. ( { z } X. [_ z / x ]_ B ) ) <-> ( x e. A /\ C e. B ) )
45	28, 44	syl6bb 185	. 2 |- ( <. x , C >. e. _V -> ( <. x , C >. e. U_ x e. A ( { x } X. B ) <-> ( x e. A /\ C e. B ) ) )
46	1, 6, 45	pm5.21nii 620	1 |- ( <. x , C >. e. U_ x e. A ( { x } X. B ) <-> ( x e. A /\ C e. B ) )

Syntax hints:   /\ wa 97   <-> wb 98   = wceq 1243   E.wex 1381   e. wcel 1393   [wsb 1645   E.wrex 2307   _Vcvv 2557   [_csb 2852   {csn 3375   <.cop 3378   U_ciun 3657   X. cxp 4343

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875  ax-pow 3927  ax-pr 3944

This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-rex 2312  df-v 2559  df-sbc 2765  df-csb 2853  df-un 2922  df-in 2924  df-ss 2931  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-iun 3659  df-opab 3819  df-xp 4351

This theorem is referenced by:  eliunxp  4475  opeliunxp2  4476