Theorem opelxp 5725

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 5713	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3482	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3482	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5491	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2827	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2827	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 638	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 217	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 250	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3199	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2735	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4878	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2746	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4879	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2746	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3635	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1449	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 209	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 275	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2106  ∃wrex 3068  ⟨cop 4637   × cxp 5687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-opab 5211  df-xp 5695

This theorem is referenced by:  opelxpi  5726  opelxp1  5731  opelxp2  5732  otelxp  5733  otel3xp  5735  brxp  5738  opthprc  5753  elxp3  5755  opeliunxp  5756  bropaex12  5780  optocl  5783  xpsspw  5822  inxp  5845  xpiindi  5849  opelres  6006  restidsing  6073  codir  6143  qfto  6144  xpnz  6181  difxp  6186  xpdifid  6190  dfco2  6267  relssdmrnOLD  6291  ressn  6307  opelf  6770  oprab4  7519  resoprab  7551  oprssdm  7614  nssdmovg  7615  ndmovg  7616  elmpocl  7674  fo1stres  8039  fo2ndres  8040  dfoprab4  8079  opiota  8083  bropopvvv  8114  bropfvvvvlem  8115  curry1  8128  xporderlem  8151  fnwelem  8155  frpoins3xpg  8164  xpord2lem  8166  xpord2pred  8169  xpord2indlem  8171  mpoxopxprcov0  8241  mpocurryd  8293  on2recsov  8705  naddcllem  8713  brecop  8849  brecop2  8850  eceqoveq  8861  xpdom2  9106  mapunen  9185  djuss  9958  djuunxp  9959  dfac5lem2  10162  iunfo  10577  ordpipq  10980  prsrlem1  11110  opelcn  11167  opelreal  11168  elreal2  11170  swrdnznd  14677  swrd00  14679  swrdcl  14680  swrd0  14693  pfx00  14709  pfx0  14710  fsumcom2  15807  fprodcom2  16017  phimullem  16813  imasvscafn  17584  homarcl2  18089  evlfcl  18279  clatl  18566  pzriprnglem4  21513  pzriprnglem9  21518  matplusgcell  22455  iscnp2  23263  txuni2  23589  txcls  23628  txcnpi  23632  txcnp  23644  txcnmpt  23648  txdis1cn  23659  txtube  23664  hausdiag  23669  txlm  23672  tx1stc  23674  txkgen  23676  txflf  24030  tmdcn2  24113  tgphaus  24141  qustgplem  24145  fmucndlem  24316  xmeterval  24458  metustexhalf  24585  blval2  24591  bcthlem1  25372  ovolfcl  25515  ovoliunlem1  25551  mbfimaopnlem  25704  limccnp2  25942  fsumvma  27272  lgsquadlem1  27439  lgsquadlem2  27440  norec2ov  28005  dmrab  32525  xppreima2  32668  aciunf1lem  32679  f1od2  32739  smatrcl  33757  smatlem  33758  qtophaus  33797  eulerpartlemgvv  34358  erdszelem10  35185  cvmlift2lem10  35297  cvmlift2lem12  35299  msubff  35515  elmpst  35521  mpstrcl  35526  elmpps  35558  dfso2  35735  fv1stcnv  35758  fv2ndcnv  35759  txpss3v  35860  dfrdg4  35933  bj-opelrelex  37127  bj-opelidres  37144  bj-elid6  37153  bj-eldiag2  37160  bj-inftyexpitaudisj  37188  curf  37585  curunc  37589  heiborlem3  37800  xrnss3v  38354  inxpxrn  38377  dibopelvalN  41126  dibopelval2  41128  dib1dim  41148  dihopcl  41236  dih1  41269  dih1dimatlem  41312  hdmap1val  41781  aks6d1c3  42105  pellex  42823  elnonrel  43575  mnringmulrcld  44224  fourierdlem42  46105  etransclem44  46234  ovn0lem  46521  ndmaovg  47134  aoprssdm  47152  ndmaovcl  47153  ndmaovrcl  47154  ndmaovcom  47155  ndmaovass  47156  ndmaovdistr  47157  sprsymrelfvlem  47415  sprsymrelfolem2  47418  prproropf1olem2  47429  opeliun2xp  48178  joindm2  48765  meetdm2  48767