Theorem opelxp 3271

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 3262	. 2 |- (<.A, B>. e. (C X. D) -> A e. C)
2		pm3.26 326	. 2 |- ((A e. C /\ B e. D) -> A e. C)
3		opeq1 2541	. . . 4 |- (z = A -> <.z, B>. = <.A, B>.)
4	3	eleq1d 1587	. . 3 |- (z = A -> (<.z, B>. e. (C X. D) <-> <.A, B>. e. (C X. D)))
5		eleq1 1581	. . . 4 |- (z = A -> (z e. C <-> A e. C))
6	5	anbi1d 628	. . 3 |- (z = A -> ((z e. C /\ B e. D) <-> (A e. C /\ B e. D)))
7		eqcom 1524	. . . . . . . . . . 11 |- (<.z, B>. = <.x, y>. <-> <.x, y>. = <.z, B>.)
8		visset 1860	. . . . . . . . . . . 12 |- x e. V
9		visset 1860	. . . . . . . . . . . 12 |- y e. V
10		opelxp.1	. . . . . . . . . . . 12 |- B e. V
11	8, 9, 10	opth 2843	. . . . . . . . . . 11 |- (<.x, y>. = <.z, B>. <-> (x = z /\ y = B))
12	7, 11	bitri 180	. . . . . . . . . 10 |- (<.z, B>. = <.x, y>. <-> (x = z /\ y = B))
13	12	anbi1i 492	. . . . . . . . 9 |- ((<.z, B>. = <.x, y>. /\ (x e. C /\ y e. D)) <-> ((x = z /\ y = B) /\ (x e. C /\ y e. D)))
14		an4 517	. . . . . . . . 9 |- (((x = z /\ y = B) /\ (x e. C /\ y e. D)) <-> ((x = z /\ x e. C) /\ (y = B /\ y e. D)))
15	13, 14	bitri 180	. . . . . . . 8 |- ((<.z, B>. = <.x, y>. /\ (x e. C /\ y e. D)) <-> ((x = z /\ x e. C) /\ (y = B /\ y e. D)))
16	15	exbii 1092	. . . . . . 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 1350	. . . . . . 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	bitri 180	. . . . . 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 1092	. . . . 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 1347	. . . . 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	bitri 180	. . . 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 3259	. . . 4 |- (<.z, B>. e. (C X. D) <-> E.xE.y(<.z, B>. = <.x, y>. /\ (x e. C /\ y e. D)))
23		df-clel 1518	. . . . 5 |- (z e. C <-> E.x(x = z /\ x e. C))
24		df-clel 1518	. . . . 5 |- (B e. D <-> E.y(y = B /\ y e. D))
25	23, 24	anbi12i 493	. . . 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	3bitr4i 190	. . 3 |- (<.z, B>. e. (C X. D) <-> (z e. C /\ B e. D))
27	4, 6, 26	vtoclbg 1895	. 2 |- (A e. C -> (<.A, B>. e. (C X. D) <-> (A e. C /\ B e. D)))
28	1, 2, 27	pm5.21nii 691	1 |- (<.A, B>. e. (C X. D) <-> (A e. C /\ B e. D))

Syntax hints:   <-> wb 153   /\ wa 230   = wceq 997   e. wcel 999  E.wex 1021  Vcvv 1858  <.cop 2463   X. cxp 3225

This theorem is referenced by:  brxp 3272  opelxpg 3273  ralxp 3275  opthprc 3278  elxp3 3281  optocl 3292  relsn 3311  ssxp 3313  xpsspw 3314  inxp 3326  opelres 3429  resiexg 3453  dfima2 3462  cnvxp 3521  xpnz 3523  ssrnres 3538  relssdr 3570  opelf 3697  dff2 3874  dff3 3875  resoprab 4067  oprssdm 4100  curry1 4156  df1st2 4184  df2nd2 4185  brecop 4367  brecop2 4368  ecopoprdm 4370  eceqopreq 4374  xpdom2 4505  xpmapenlem4 4564  xpmapenlem5 4565  mapunen 4567  aceq5lem2 4798  ltpiord 5080  opelcn 5313  opelreal 5314  ruclem13 7614  infxpidmlem5 7648  infxpidmlem7 7650  xplmi 8058  bcthlem32 8115  nvvop 8312  stcat 10538

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-sep 2758  ax-pow 2798  ax-pr 2835

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-v 1859  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2454  df-sn 2464  df-pr 2465  df-op 2468  df-opab 2722  df-xp 3241

Copyright terms: Public domain