Theorem opelxp 5667

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 5655	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3433	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3433	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5433	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2824	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2824	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 639	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 217	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 250	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3179	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2736	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4816	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2747	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4817	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2747	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3577	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1453	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 209	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 275	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃wrex 3061  ⟨cop 4573   × cxp 5629

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-opab 5148  df-xp 5637

This theorem is referenced by:  opelxpi  5668  opelxp1  5673  opelxp2  5674  otelxp  5675  otel3xp  5677  brxp  5680  opthprc  5695  elxp3  5697  opeliunxp  5698  opeliun2xp  5699  bropaex12  5722  optoclOLD  5726  xpsspw  5765  inxp  5787  xpiindi  5790  opelres  5950  restidsing  6018  codir  6083  qfto  6084  xpnz  6123  difxp  6128  xpdifid  6132  dfco2  6209  ressn  6249  opelf  6701  oprab4  7453  resoprab  7485  oprssdm  7548  nssdmovg  7549  ndmovg  7550  elmpocl  7608  fo1stres  7968  fo2ndres  7969  dfoprab4  8008  opiota  8012  bropopvvv  8040  bropfvvvvlem  8041  curry1  8054  xporderlem  8077  fnwelem  8081  frpoins3xpg  8090  xpord2lem  8092  xpord2pred  8095  xpord2indlem  8097  mpoxopxprcov0  8167  mpocurryd  8219  on2recsov  8604  naddcllem  8612  brecop  8757  brecop2  8758  eceqoveq  8769  xpdom2  9010  mapunen  9084  djuss  9844  djuunxp  9845  dfac5lem2  10046  iunfo  10461  ordpipq  10865  prsrlem1  10995  opelcn  11052  opelreal  11053  elreal2  11055  swrdnznd  14605  swrd00  14607  swrdcl  14608  swrd0  14621  pfx00  14637  pfx0  14638  fsumcom2  15736  fprodcom2  15949  phimullem  16749  imasvscafn  17501  homarcl2  18002  evlfcl  18188  clatl  18474  pzriprnglem4  21464  pzriprnglem9  21469  matplusgcell  22398  iscnp2  23204  txuni2  23530  txcls  23569  txcnpi  23573  txcnp  23585  txcnmpt  23589  txdis1cn  23600  txtube  23605  hausdiag  23610  txlm  23613  tx1stc  23615  txkgen  23617  txflf  23971  tmdcn2  24054  tgphaus  24082  qustgplem  24086  fmucndlem  24255  xmeterval  24397  metustexhalf  24521  blval2  24527  bcthlem1  25291  ovolfcl  25433  ovoliunlem1  25469  mbfimaopnlem  25622  limccnp2  25859  fsumvma  27176  lgsquadlem1  27343  lgsquadlem2  27344  norec2ov  27949  dmrab  32566  xppreima2  32724  aciunf1lem  32735  f1od2  32792  smatrcl  33940  smatlem  33941  qtophaus  33980  eulerpartlemgvv  34520  erdszelem10  35382  cvmlift2lem10  35494  cvmlift2lem12  35496  msubff  35712  elmpst  35718  mpstrcl  35723  elmpps  35755  dfso2  35937  fv1stcnv  35959  fv2ndcnv  35960  txpss3v  36058  dfrdg4  36133  bj-opelrelex  37458  bj-opelidres  37475  bj-elid6  37484  bj-eldiag2  37491  bj-inftyexpitaudisj  37519  curf  37919  curunc  37923  heiborlem3  38134  xrnss3v  38702  ecxrn2  38729  inxpxrn  38739  dibopelvalN  41589  dibopelval2  41591  dib1dim  41611  dihopcl  41699  dih1  41732  dih1dimatlem  41775  hdmap1val  42244  aks6d1c3  42562  pellex  43263  elnonrel  44012  mnringmulrcld  44655  fourierdlem42  46577  etransclem44  46706  ovn0lem  46993  ndmaovg  47632  aoprssdm  47650  ndmaovcl  47651  ndmaovrcl  47652  ndmaovcom  47653  ndmaovass  47654  ndmaovdistr  47655  sprsymrelfvlem  47950  sprsymrelfolem2  47953  prproropf1olem2  47964  opgpgvtx  48531  iinxp  49306  coxp  49308  joindm2  49443  meetdm2  49445  swapf2fval  49740  swapf1val  49742  fuco2el  49787