Theorem opelxp 5669

Description: Ordered pair membership in a Cartesian product. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)

Assertion

Ref	Expression
opelxp	⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Proof of Theorem opelxp

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elxp2 5657	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3449	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3449	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5437	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2825	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2825	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 637	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 216	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 249	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3196	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2736	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4830	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2747	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4831	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2747	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3592	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1450	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 208	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 274	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∃wrex 3073  ⟨cop 4592   × cxp 5631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-opab 5168  df-xp 5639

This theorem is referenced by:  opelxpi  5670  opelxp1  5674  opelxp2  5675  otelxp  5676  otel3xp  5678  brxp  5681  opthprc  5696  elxp3  5698  opeliunxp  5699  bropaex12  5723  optocl  5726  xpsspw  5765  xpiindi  5791  opelres  5943  restidsing  6006  codir  6074  qfto  6075  xpnz  6111  difxp  6116  xpdifid  6120  dfco2  6197  relssdmrnOLD  6221  ressn  6237  opelf  6703  oprab4  7443  resoprab  7474  oprssdm  7535  nssdmovg  7536  ndmovg  7537  elmpocl  7595  fo1stres  7947  fo2ndres  7948  dfoprab4  7987  opiota  7991  bropopvvv  8022  bropfvvvvlem  8023  curry1  8036  xporderlem  8059  fnwelem  8063  frpoins3xpg  8072  xpord2lem  8074  xpord2pred  8077  xpord2indlem  8079  mpoxopxprcov0  8148  mpocurryd  8200  on2recsov  8614  naddcllem  8622  brecop  8749  brecop2  8750  eceqoveq  8761  xpdom2  9011  mapunen  9090  djuss  9856  djuunxp  9857  dfac5lem2  10060  iunfo  10475  ordpipq  10878  prsrlem1  11008  opelcn  11065  opelreal  11066  elreal2  11068  swrdnznd  14530  swrd00  14532  swrdcl  14533  swrd0  14546  pfx00  14562  pfx0  14563  fsumcom2  15659  fprodcom2  15867  phimullem  16651  imasvscafn  17419  homarcl2  17921  evlfcl  18111  clatl  18397  matplusgcell  21782  iscnp2  22590  txuni2  22916  txcls  22955  txcnpi  22959  txcnp  22971  txcnmpt  22975  txdis1cn  22986  txtube  22991  hausdiag  22996  txlm  22999  tx1stc  23001  txkgen  23003  txflf  23357  tmdcn2  23440  tgphaus  23468  qustgplem  23472  fmucndlem  23643  xmeterval  23785  metustexhalf  23912  blval2  23918  bcthlem1  24688  ovolfcl  24830  ovoliunlem1  24866  mbfimaopnlem  25019  limccnp2  25256  fsumvma  26561  lgsquadlem1  26728  lgsquadlem2  26729  norec2ov  27269  dmrab  31425  xppreima2  31567  aciunf1lem  31578  f1od2  31638  smatrcl  32377  smatlem  32378  qtophaus  32417  eulerpartlemgvv  32976  erdszelem10  33794  cvmlift2lem10  33906  cvmlift2lem12  33908  msubff  34124  elmpst  34130  mpstrcl  34135  elmpps  34167  dfso2  34328  fv1stcnv  34351  fv2ndcnv  34352  txpss3v  34463  dfrdg4  34536  bj-opelrelex  35615  bj-opelidres  35632  bj-elid6  35641  bj-eldiag2  35648  bj-inftyexpitaudisj  35676  curf  36056  curunc  36060  heiborlem3  36272  xrnss3v  36834  inxpxrn  36857  dibopelvalN  39606  dibopelval2  39608  dib1dim  39628  dihopcl  39716  dih1  39749  dih1dimatlem  39792  hdmap1val  40261  pellex  41144  elnonrel  41847  mnringmulrcld  42498  fourierdlem42  44380  etransclem44  44509  ovn0lem  44796  ndmaovg  45406  aoprssdm  45424  ndmaovcl  45425  ndmaovrcl  45426  ndmaovcom  45427  ndmaovass  45428  ndmaovdistr  45429  sprsymrelfvlem  45672  sprsymrelfolem2  45675  prproropf1olem2  45686  opeliun2xp  46398  joindm2  46991  meetdm2  46993