Theorem opelxp 5687

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 5675	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3454	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3454	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5449	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2848	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2848	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 650	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 220	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 253	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3204	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2760	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4839	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2771	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4840	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2771	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3588	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1479	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 212	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 278	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ∃wrex 3086  ⟨cop 4834   × cxp 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-opab 5167  df-xp 5657

This theorem is used by:  opelxpi  5688  opelxp1  5693  opelxp2  5694  otelxp  5695  otel3xp  5697  brxp  5700  opthprc  5715  elxp3  5717  opeliunxp  5718  opeliun2xp  5719  bropaex12  5743  optoclOLD  5747  xpsspw  5788  inxp  5810  xpiindi  5813  opelres  5977  restidsing  6047  codir  6116  qfto  6117  xpnz  6152  difxp  6157  xpdifid  6161  xpdifcnvepel  6162  dfco2  6249  ressn  6291  opelf  6748  oprab4  7510  resoprab  7542  oprssdm  7606  nssdmovg  7607  ndmovg  7608  elmpocl  7666  fo1stres  8031  fo2ndres  8032  dfoprab4  8071  opiota  8075  bropopvvv  8106  bropfvvvvlem  8107  f1od2  8115  curry1  8122  xporderlem  8146  fnwelem  8150  frpoins3xpg  8164  xpord2lem  8166  xpord2pred  8169  xpord2indlem  8171  mpoxopxprcov0  8242  mpocurryd  8294  on2recsov  8685  naddcllem  8693  brecop  8839  brecop2  8840  eceqoveq  8851  curf  8898  xpdom2  9099  mapunen  9173  djuss  10008  djuunxp  10009  dfac5lem2  10210  iunfo  10630  ordpipq  11034  prsrlem1  11164  opelcn  11221  opelreal  11222  elreal2  11224  swrdnznd  14798  swrd00  14800  swrdcl  14801  swrd0  14816  pfx00  14832  pfx0  14833  fsumcom2  15949  fprodcom2  16160  phimullem  16965  imasvscafn  17718  homarcl2  18219  evlfcl  18405  clatl  18691  pzriprnglem4  21799  pzriprnglem9  21804  matplusgcell  22757  iscnp2  23566  txuni2  23893  txcls  23932  txcnpi  23936  txcnp  23948  txcnmpt  23952  txdis1cn  23963  txtube  23968  hausdiag  23973  txlm  23976  tx1stc  23978  txkgen  23980  txflf  24334  tmdcn2  24417  tgphaus  24445  qustgplem  24449  fmucndlem  24618  xmeterval  24760  metustexhalf  24884  blval2  24890  bcthlem1  25654  ovolfcl  25796  ovoliunlem1  25832  mbfimaopnlem  25985  limccnp2  26221  fsumvma  27549  lgsquadlem1  27716  lgsquadlem2  27717  norec2ov  28352  dmrab  33144  xppreima2  33296  aciunf1lem  33307  smatrcl  34478  smatlem  34479  qtophaus  34518  eulerpartlemgvv  35058  erdszelem10  36083  cvmlift2lem10  36195  cvmlift2lem12  36197  msubff  36413  elmpst  36419  mpstrcl  36424  elmpps  36456  dfso2  36644  fv1stcnv  36665  fv2ndcnv  36666  txpss3v  36764  dfrdg4  36839  bj-opelrelex  38202  bj-opelidres  38219  bj-elid6  38228  bj-eldiag2  38235  bj-inftyexpitaudisj  38263  curunc  38662  heiborlem3  38884  xrnss3v  39450  ecxrn2  39477  inxpxrn  39487  dibopelvalN  42337  dibopelval2  42339  dib1dim  42359  dihopcl  42447  dih1  42480  dih1dimatlem  42523  hdmap1val  42992  aks6d1c3  43310  pellex  43979  elnonrel  44723  mnringmulrcld  45363  fourierdlem42  47295  etransclem44  47424  ovn0lem  47711  ndmaovg  48390  aoprssdm  48408  ndmaovcl  48409  ndmaovrcl  48410  ndmaovcom  48411  ndmaovass  48412  ndmaovdistr  48413  sprsymrelfvlem  48708  sprsymrelfolem2  48711  prproropf1olem2  48722  opgpgvtx  49289  iinxp  50078  coxp  50080  joindm2  50218  meetdm2  50220  swapf2fval  50523  swapf1val  50525  fuco2el  50570