Theorem opelxp 5691

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 5679	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3454	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3454	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5456	. . . . . 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 4833	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2771	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4834	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2771	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3589	. . . 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 1570   ∈ wcel 2145  ∃wrex 3086  ⟨cop 4590   × cxp 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-opab 5168  df-xp 5661

This theorem is used by:  opelxpi  5692  opelxp1  5697  opelxp2  5698  otelxp  5699  otel3xp  5701  brxp  5704  opthprc  5719  elxp3  5721  opeliunxp  5722  opeliun2xp  5723  bropaex12  5746  optoclOLD  5750  xpsspw  5790  inxp  5812  xpiindi  5815  opelres  5978  restidsing  6049  codir  6114  qfto  6115  xpnz  6151  difxp  6156  xpdifid  6160  xpdifcnvepel  6161  dfco2  6241  ressn  6283  opelf  6737  oprab4  7500  resoprab  7532  oprssdm  7596  nssdmovg  7597  ndmovg  7598  elmpocl  7656  fo1stres  8013  fo2ndres  8014  dfoprab4  8053  opiota  8057  bropopvvv  8088  bropfvvvvlem  8089  curry1  8102  xporderlem  8126  fnwelem  8130  frpoins3xpg  8139  xpord2lem  8141  xpord2pred  8144  xpord2indlem  8146  mpoxopxprcov0  8216  mpocurryd  8268  on2recsov  8657  naddcllem  8665  brecop  8811  brecop2  8812  eceqoveq  8823  curf  8870  xpdom2  9071  mapunen  9145  djuss  9926  djuunxp  9927  dfac5lem2  10128  iunfo  10548  ordpipq  10952  prsrlem1  11082  opelcn  11139  opelreal  11140  elreal2  11142  swrdnznd  14711  swrd00  14713  swrdcl  14714  swrd0  14729  pfx00  14745  pfx0  14746  fsumcom2  15861  fprodcom2  16072  phimullem  16871  imasvscafn  17624  homarcl2  18125  evlfcl  18311  clatl  18597  pzriprnglem4  21698  pzriprnglem9  21703  matplusgcell  22656  iscnp2  23465  txuni2  23792  txcls  23831  txcnpi  23835  txcnp  23847  txcnmpt  23851  txdis1cn  23862  txtube  23867  hausdiag  23872  txlm  23875  tx1stc  23877  txkgen  23879  txflf  24233  tmdcn2  24316  tgphaus  24344  qustgplem  24348  fmucndlem  24517  xmeterval  24659  metustexhalf  24783  blval2  24789  bcthlem1  25553  ovolfcl  25695  ovoliunlem1  25731  mbfimaopnlem  25884  limccnp2  26120  fsumvma  27450  lgsquadlem1  27617  lgsquadlem2  27618  norec2ov  28223  dmrab  32973  xppreima2  33125  aciunf1lem  33136  f1od2  33191  smatrcl  34307  smatlem  34308  qtophaus  34347  eulerpartlemgvv  34888  erdszelem10  35780  cvmlift2lem10  35892  cvmlift2lem12  35894  msubff  36110  elmpst  36116  mpstrcl  36121  elmpps  36153  dfso2  36335  fv1stcnv  36357  fv2ndcnv  36358  txpss3v  36456  dfrdg4  36531  bj-opelrelex  37897  bj-opelidres  37914  bj-elid6  37923  bj-eldiag2  37930  bj-inftyexpitaudisj  37958  curunc  38357  heiborlem3  38564  xrnss3v  39130  ecxrn2  39157  inxpxrn  39167  dibopelvalN  42017  dibopelval2  42019  dib1dim  42039  dihopcl  42127  dih1  42160  dih1dimatlem  42203  hdmap1val  42672  aks6d1c3  42990  pellex  43677  elnonrel  44426  mnringmulrcld  45067  fourierdlem42  46978  etransclem44  47107  ovn0lem  47394  ndmaovg  48073  aoprssdm  48091  ndmaovcl  48092  ndmaovrcl  48093  ndmaovcom  48094  ndmaovass  48095  ndmaovdistr  48096  sprsymrelfvlem  48391  sprsymrelfolem2  48394  prproropf1olem2  48405  opgpgvtx  48972  iinxp  49760  coxp  49762  joindm2  49895  meetdm2  49897  swapf2fval  50192  swapf1val  50194  fuco2el  50239