Theorem opelxp 5654

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 5642	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3435	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3435	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5420	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2827	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2827	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 644	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 218	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 251	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3181	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2739	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4804	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2750	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4805	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2750	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3573	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1458	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 210	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 276	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∃wrex 3063  ⟨cop 4561   × cxp 5616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-opab 5135  df-xp 5624

This theorem is referenced by:  opelxpi  5655  opelxp1  5660  opelxp2  5661  otelxp  5662  otel3xp  5664  brxp  5667  opthprc  5682  elxp3  5684  opeliunxp  5685  opeliun2xp  5686  bropaex12  5709  optoclOLD  5713  xpsspw  5752  inxp  5774  xpiindi  5777  opelres  5937  restidsing  6005  codir  6070  qfto  6071  xpnz  6110  difxp  6115  xpdifid  6119  dfco2  6196  ressn  6236  opelf  6688  oprab4  7442  resoprab  7474  oprssdm  7537  nssdmovg  7538  ndmovg  7539  elmpocl  7597  fo1stres  7957  fo2ndres  7958  dfoprab4  7997  opiota  8001  bropopvvv  8029  bropfvvvvlem  8030  curry1  8043  xporderlem  8067  fnwelem  8071  frpoins3xpg  8080  xpord2lem  8082  xpord2pred  8085  xpord2indlem  8087  mpoxopxprcov0  8157  mpocurryd  8209  on2recsov  8594  naddcllem  8602  brecop  8747  brecop2  8748  eceqoveq  8759  xpdom2  9000  mapunen  9074  djuss  9835  djuunxp  9836  dfac5lem2  10037  iunfo  10452  ordpipq  10856  prsrlem1  10986  opelcn  11043  opelreal  11044  elreal2  11046  swrdnznd  14596  swrd00  14598  swrdcl  14599  swrd0  14612  pfx00  14628  pfx0  14629  fsumcom2  15727  fprodcom2  15940  phimullem  16740  imasvscafn  17492  homarcl2  17993  evlfcl  18179  clatl  18465  pzriprnglem4  21459  pzriprnglem9  21464  matplusgcell  22416  iscnp2  23222  txuni2  23548  txcls  23587  txcnpi  23591  txcnp  23603  txcnmpt  23607  txdis1cn  23618  txtube  23623  hausdiag  23628  txlm  23631  tx1stc  23633  txkgen  23635  txflf  23989  tmdcn2  24072  tgphaus  24100  qustgplem  24104  fmucndlem  24273  xmeterval  24415  metustexhalf  24539  blval2  24545  bcthlem1  25309  ovolfcl  25451  ovoliunlem1  25487  mbfimaopnlem  25640  limccnp2  25877  fsumvma  27194  lgsquadlem1  27361  lgsquadlem2  27362  norec2ov  27967  dmrab  32584  xppreima2  32743  aciunf1lem  32754  f1od2  32811  smatrcl  33980  smatlem  33981  qtophaus  34020  eulerpartlemgvv  34560  erdszelem10  35428  cvmlift2lem10  35540  cvmlift2lem12  35542  msubff  35758  elmpst  35764  mpstrcl  35769  elmpps  35801  dfso2  35983  fv1stcnv  36005  fv2ndcnv  36006  txpss3v  36104  dfrdg4  36179  bj-opelrelex  37504  bj-opelidres  37521  bj-elid6  37530  bj-eldiag2  37537  bj-inftyexpitaudisj  37565  curf  37965  curunc  37969  heiborlem3  38180  xrnss3v  38748  ecxrn2  38775  inxpxrn  38785  dibopelvalN  41635  dibopelval2  41637  dib1dim  41657  dihopcl  41745  dih1  41778  dih1dimatlem  41821  hdmap1val  42290  aks6d1c3  42608  pellex  43280  elnonrel  44029  mnringmulrcld  44672  fourierdlem42  46592  etransclem44  46721  ovn0lem  47008  ndmaovg  47647  aoprssdm  47665  ndmaovcl  47666  ndmaovrcl  47667  ndmaovcom  47668  ndmaovass  47669  ndmaovdistr  47670  sprsymrelfvlem  47965  sprsymrelfolem2  47968  prproropf1olem2  47979  opgpgvtx  48546  iinxp  49321  coxp  49323  joindm2  49458  meetdm2  49460  swapf2fval  49755  swapf1val  49757  fuco2el  49802