Theorem opelxp 3209

Description: Ordered pair membership in a cross product.

Hypothesis

Ref	Expression
opelxp.1	|- B e. V

Assertion

Ref	Expression
opelxp	|- (<.A, B>. e. (C X. D) <-> (A e. C /\ B e. D))

Proof of Theorem opelxp

Step	Hyp	Ref	Expression
1		opelxp1 3200	. 2 |- (<.A, B>. e. (C X. D) -> A e. C)
2		pm3.26 319	. 2 |- ((A e. C /\ B e. D) -> A e. C)
3		opeq1 2483	. . . 4 |- (z = A -> <.z, B>. = <.A, B>.)
4	3	eleq1d 1537	. . 3 |- (z = A -> (<.z, B>. e. (C X. D) <-> <.A, B>. e. (C X. D)))
5		eleq1 1531	. . . 4 |- (z = A -> (z e. C <-> A e. C))
6	5	anbi1d 616	. . 3 |- (z = A -> ((z e. C /\ B e. D) <-> (A e. C /\ B e. D)))
7		eqcom 1474	. . . . . . . . . . 11 |- (<.z, B>. = <.x, y>. <-> <.x, y>. = <.z, B>.)
8		visset 1809	. . . . . . . . . . . 12 |- x e. V
9		visset 1809	. . . . . . . . . . . 12 |- y e. V
10		opelxp.1	. . . . . . . . . . . 12 |- B e. V
11	8, 9, 10	opth 2782	. . . . . . . . . . 11 |- (<.x, y>. = <.z, B>. <-> (x = z /\ y = B))
12	7, 11	bitr 173	. . . . . . . . . 10 |- (<.z, B>. = <.x, y>. <-> (x = z /\ y = B))
13	12	anbi1i 481	. . . . . . . . 9 |- ((<.z, B>. = <.x, y>. /\ (x e. C /\ y e. D)) <-> ((x = z /\ y = B) /\ (x e. C /\ y e. D)))
14		an4 506	. . . . . . . . 9 |- (((x = z /\ y = B) /\ (x e. C /\ y e. D)) <-> ((x = z /\ x e. C) /\ (y = B /\ y e. D)))
15	13, 14	bitr 173	. . . . . . . 8 |- ((<.z, B>. = <.x, y>. /\ (x e. C /\ y e. D)) <-> ((x = z /\ x e. C) /\ (y = B /\ y e. D)))
16	15	exbii 1049	. . . . . . 7 |- (E.y(<.z, B>. = <.x, y>. /\ (x e. C /\ y e. D)) <-> E.y((x = z /\ x e. C) /\ (y = B /\ y e. D)))
17		19.42v 1306	. . . . . . 7 |- (E.y((x = z /\ x e. C) /\ (y = B /\ y e. D)) <-> ((x = z /\ x e. C) /\ E.y(y = B /\ y e. D)))
18	16, 17	bitr 173	. . . . . 6 |- (E.y(<.z, B>. = <.x, y>. /\ (x e. C /\ y e. D)) <-> ((x = z /\ x e. C) /\ E.y(y = B /\ y e. D)))
19	18	exbii 1049	. . . . 5 |- (E.xE.y(<.z, B>. = <.x, y>. /\ (x e. C /\ y e. D)) <-> E.x((x = z /\ x e. C) /\ E.y(y = B /\ y e. D)))
20		19.41v 1303	. . . . 5 |- (E.x((x = z /\ x e. C) /\ E.y(y = B /\ y e. D)) <-> (E.x(x = z /\ x e. C) /\ E.y(y = B /\ y e. D)))
21	19, 20	bitr 173	. . . 4 |- (E.xE.y(<.z, B>. = <.x, y>. /\ (x e. C /\ y e. D)) <-> (E.x(x = z /\ x e. C) /\ E.y(y = B /\ y e. D)))
22		elxp 3197	. . . 4 |- (<.z, B>. e. (C X. D) <-> E.xE.y(<.z, B>. = <.x, y>. /\ (x e. C /\ y e. D)))
23		df-clel 1470	. . . . 5 |- (z e. C <-> E.x(x = z /\ x e. C))
24		df-clel 1470	. . . . 5 |- (B e. D <-> E.y(y = B /\ y e. D))
25	23, 24	anbi12i 482	. . . 4 |- ((z e. C /\ B e. D) <-> (E.x(x = z /\ x e. C) /\ E.y(y = B /\ y e. D)))
26	21, 22, 25	3bitr4 183	. . 3 |- (<.z, B>. e. (C X. D) <-> (z e. C /\ B e. D))
27	4, 6, 26	vtoclbg 1844	. 2 |- (A e. C -> (<.A, B>. e. (C X. D) <-> (A e. C /\ B e. D)))
28	1, 2, 27	pm5.21nii 678	1 |- (<.A, B>. e. (C X. D) <-> (A e. C /\ B e. D))

Syntax hints:   <-> wb 146   /\ wa 223   = wceq 954   e. wcel 956  E.wex 978  Vcvv 1807  <.cop 2407   X. cxp 3163

This theorem is referenced by:  brxp 3210  opelxpg 3211  ralxp 3213  opthprc 3216  elxp3 3219  optocl 3230  relsn 3249  ssxp 3251  xpsspw 3252  inxp 3264  opelres 3364  resiexg 3388  dfima2 3397  cnvxp 3456  xpnz 3458  ssrnres 3473  relssdr 3505  opelf 3631  dff2 3808  dff3 3809  resoprab 4000  oprssdm 4033  curry1 4088  df1st2 4116  df2nd2 4117  brecop 4296  brecop2 4297  ecopoprdm 4299  eceqopreq 4303  xpdom2 4428  xpmapenlem4 4485  xpmapenlem5 4486  mapunen 4488  aceq5lem2 4716  ltpiord 4995  opelcn 5228  opelreal 5229  ruclem13 7473  infxpidmlem5 7507  infxpidmlem7 7509  xplmi 7923  bcthlem32 7980  nvvop 8180  stcat 10389

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737  ax-pr 2774

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-op 2412  df-opab 2662  df-xp 3179

Copyright terms: Public domain