Theorem opelxp 5713

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 5701	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3476	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3476	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5481	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2819	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2819	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 635	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 216	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 249	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3197	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2730	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4874	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2741	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4875	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2741	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3625	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1448	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 208	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 274	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 205   ∧ wa 394   = wceq 1539   ∈ wcel 2104  ∃wrex 3068  ⟨cop 4635   × cxp 5675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-opab 5212  df-xp 5683

This theorem is referenced by:  opelxpi  5714  opelxp1  5719  opelxp2  5720  otelxp  5721  otel3xp  5723  brxp  5726  opthprc  5741  elxp3  5743  opeliunxp  5744  bropaex12  5768  optocl  5771  xpsspw  5810  xpiindi  5836  opelres  5988  restidsing  6053  codir  6122  qfto  6123  xpnz  6159  difxp  6164  xpdifid  6168  dfco2  6245  relssdmrnOLD  6269  ressn  6285  opelf  6753  oprab4  7499  resoprab  7530  oprssdm  7592  nssdmovg  7593  ndmovg  7594  elmpocl  7652  fo1stres  8005  fo2ndres  8006  dfoprab4  8045  opiota  8049  bropopvvv  8080  bropfvvvvlem  8081  curry1  8094  xporderlem  8117  fnwelem  8121  frpoins3xpg  8130  xpord2lem  8132  xpord2pred  8135  xpord2indlem  8137  mpoxopxprcov0  8206  mpocurryd  8258  on2recsov  8671  naddcllem  8679  brecop  8808  brecop2  8809  eceqoveq  8820  xpdom2  9071  mapunen  9150  djuss  9919  djuunxp  9920  dfac5lem2  10123  iunfo  10538  ordpipq  10941  prsrlem1  11071  opelcn  11128  opelreal  11129  elreal2  11131  swrdnznd  14598  swrd00  14600  swrdcl  14601  swrd0  14614  pfx00  14630  pfx0  14631  fsumcom2  15726  fprodcom2  15934  phimullem  16718  imasvscafn  17489  homarcl2  17991  evlfcl  18181  clatl  18467  pzriprnglem4  21255  pzriprnglem9  21260  matplusgcell  22157  iscnp2  22965  txuni2  23291  txcls  23330  txcnpi  23334  txcnp  23346  txcnmpt  23350  txdis1cn  23361  txtube  23366  hausdiag  23371  txlm  23374  tx1stc  23376  txkgen  23378  txflf  23732  tmdcn2  23815  tgphaus  23843  qustgplem  23847  fmucndlem  24018  xmeterval  24160  metustexhalf  24287  blval2  24293  bcthlem1  25074  ovolfcl  25217  ovoliunlem1  25253  mbfimaopnlem  25406  limccnp2  25643  fsumvma  26950  lgsquadlem1  27117  lgsquadlem2  27118  norec2ov  27677  dmrab  32002  xppreima2  32141  aciunf1lem  32152  f1od2  32211  smatrcl  33072  smatlem  33073  qtophaus  33112  eulerpartlemgvv  33671  erdszelem10  34487  cvmlift2lem10  34599  cvmlift2lem12  34601  msubff  34817  elmpst  34823  mpstrcl  34828  elmpps  34860  dfso2  35027  fv1stcnv  35050  fv2ndcnv  35051  txpss3v  35152  dfrdg4  35225  bj-opelrelex  36330  bj-opelidres  36347  bj-elid6  36356  bj-eldiag2  36363  bj-inftyexpitaudisj  36391  curf  36771  curunc  36775  heiborlem3  36986  xrnss3v  37547  inxpxrn  37570  dibopelvalN  40319  dibopelval2  40321  dib1dim  40341  dihopcl  40429  dih1  40462  dih1dimatlem  40505  hdmap1val  40974  pellex  41877  elnonrel  42640  mnringmulrcld  43291  fourierdlem42  45165  etransclem44  45294  ovn0lem  45581  ndmaovg  46192  aoprssdm  46210  ndmaovcl  46211  ndmaovrcl  46212  ndmaovcom  46213  ndmaovass  46214  ndmaovdistr  46215  sprsymrelfvlem  46458  sprsymrelfolem2  46461  prproropf1olem2  46472  opeliun2xp  47098  joindm2  47690  meetdm2  47692