Theorem opelxp 5655

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 5643	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3440	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3440	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5423	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2816	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2816	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 638	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 217	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 250	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3171	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2729	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4824	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2740	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4825	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2740	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3590	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1452	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 209	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 275	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∃wrex 3053  ⟨cop 4583   × cxp 5617

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-opab 5155  df-xp 5625

This theorem is referenced by:  opelxpi  5656  opelxp1  5661  opelxp2  5662  otelxp  5663  otel3xp  5665  brxp  5668  opthprc  5683  elxp3  5685  opeliunxp  5686  opeliun2xp  5687  bropaex12  5710  optoclOLD  5714  xpsspw  5752  inxp  5774  xpiindi  5778  opelres  5936  restidsing  6004  codir  6069  qfto  6070  xpnz  6108  difxp  6113  xpdifid  6117  dfco2  6194  ressn  6233  opelf  6685  oprab4  7435  resoprab  7467  oprssdm  7530  nssdmovg  7531  ndmovg  7532  elmpocl  7590  fo1stres  7950  fo2ndres  7951  dfoprab4  7990  opiota  7994  bropopvvv  8023  bropfvvvvlem  8024  curry1  8037  xporderlem  8060  fnwelem  8064  frpoins3xpg  8073  xpord2lem  8075  xpord2pred  8078  xpord2indlem  8080  mpoxopxprcov0  8150  mpocurryd  8202  on2recsov  8586  naddcllem  8594  brecop  8737  brecop2  8738  eceqoveq  8749  xpdom2  8989  mapunen  9063  djuss  9816  djuunxp  9817  dfac5lem2  10018  iunfo  10433  ordpipq  10836  prsrlem1  10966  opelcn  11023  opelreal  11024  elreal2  11026  swrdnznd  14549  swrd00  14551  swrdcl  14552  swrd0  14565  pfx00  14581  pfx0  14582  fsumcom2  15681  fprodcom2  15891  phimullem  16690  imasvscafn  17441  homarcl2  17942  evlfcl  18128  clatl  18414  pzriprnglem4  21391  pzriprnglem9  21396  matplusgcell  22318  iscnp2  23124  txuni2  23450  txcls  23489  txcnpi  23493  txcnp  23505  txcnmpt  23509  txdis1cn  23520  txtube  23525  hausdiag  23530  txlm  23533  tx1stc  23535  txkgen  23537  txflf  23891  tmdcn2  23974  tgphaus  24002  qustgplem  24006  fmucndlem  24176  xmeterval  24318  metustexhalf  24442  blval2  24448  bcthlem1  25222  ovolfcl  25365  ovoliunlem1  25401  mbfimaopnlem  25554  limccnp2  25791  fsumvma  27122  lgsquadlem1  27289  lgsquadlem2  27290  norec2ov  27869  dmrab  32441  xppreima2  32594  aciunf1lem  32605  f1od2  32663  smatrcl  33763  smatlem  33764  qtophaus  33803  eulerpartlemgvv  34344  erdszelem10  35177  cvmlift2lem10  35289  cvmlift2lem12  35291  msubff  35507  elmpst  35513  mpstrcl  35518  elmpps  35550  dfso2  35732  fv1stcnv  35754  fv2ndcnv  35755  txpss3v  35856  dfrdg4  35929  bj-opelrelex  37122  bj-opelidres  37139  bj-elid6  37148  bj-eldiag2  37155  bj-inftyexpitaudisj  37183  curf  37582  curunc  37586  heiborlem3  37797  xrnss3v  38344  inxpxrn  38371  dibopelvalN  41126  dibopelval2  41128  dib1dim  41148  dihopcl  41236  dih1  41269  dih1dimatlem  41312  hdmap1val  41781  aks6d1c3  42100  pellex  42812  elnonrel  43562  mnringmulrcld  44205  fourierdlem42  46134  etransclem44  46263  ovn0lem  46550  ndmaovg  47172  aoprssdm  47190  ndmaovcl  47191  ndmaovrcl  47192  ndmaovcom  47193  ndmaovass  47194  ndmaovdistr  47195  sprsymrelfvlem  47478  sprsymrelfolem2  47481  prproropf1olem2  47492  opgpgvtx  48043  iinxp  48819  coxp  48821  joindm2  48956  meetdm2  48958  swapf2fval  49254  swapf1val  49256  fuco2el  49301