Theorem opelxp 5694

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 5682	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3458	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3458	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5456	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2852	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2852	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 650	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 220	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 253	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3208	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2763	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4845	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2774	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4846	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2774	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3592	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1480	. . 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 2147  ∃wrex 3090  ⟨cop 4840   × cxp 5656

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-opab 5174  df-xp 5664

This theorem is used by:  opelxpi  5695  opelxp1  5700  opelxp2  5701  otelxp  5702  otel3xp  5704  brxp  5707  opthprc  5722  elxp3  5724  opeliunxp  5725  opeliun2xp  5726  bropaex12  5750  optoclOLD  5754  xpsspw  5796  inxp  5819  xpiindi  5822  opelres  5992  restidsing  6063  codir  6132  qfto  6133  xpnz  6168  difxp  6173  xpdifid  6177  xpdifcnvepel  6178  dfco2  6265  ressn  6312  opelf  6773  oprab4  7537  resoprab  7569  oprssdm  7634  nssdmovg  7635  ndmovg  7636  elmpocl  7694  fo1stres  8061  fo2ndres  8062  dfoprab4  8101  opiota  8105  bropopvvv  8136  bropfvvvvlem  8137  f1od2  8145  curry1  8152  xporderlem  8176  fnwelem  8180  frpoins3xpg  8194  xpord2lem  8196  xpord2pred  8199  xpord2indlem  8201  mpoxopxprcov0  8272  mpocurryd  8324  on2recsov  8715  naddcllem  8723  brecop  8869  brecop2  8870  eceqoveq  8881  curf  8928  xpdom2  9129  mapunen  9203  djuss  10038  djuunxp  10039  dfac5lem2  10242  iunfo  10662  ordpipq  11066  prsrlem1  11196  opelcn  11253  opelreal  11254  elreal2  11256  swrdnznd  14832  swrd00  14834  swrdcl  14835  swrd0  14850  pfx00  14866  pfx0  14867  fsumcom2  15984  fprodcom2  16195  phimullem  17000  imasvscafn  17759  homarcl2  18260  evlfcl  18446  clatl  18732  pzriprnglem4  21845  pzriprnglem9  21850  matplusgcell  22803  iscnp2  23612  txuni2  23939  txcls  23978  txcnpi  23982  txcnp  23994  txcnmpt  23998  txdis1cn  24009  txtube  24014  hausdiag  24019  txlm  24022  tx1stc  24024  txkgen  24026  txflf  24380  tmdcn2  24463  tgphaus  24491  qustgplem  24495  fmucndlem  24664  xmeterval  24806  metustexhalf  24930  blval2  24936  bcthlem1  25700  ovolfcl  25842  ovoliunlem1  25878  mbfimaopnlem  26031  limccnp2  26267  fsumvma  27597  lgsquadlem1  27764  lgsquadlem2  27765  norec2ov  28400  dmrab  33192  xppreima2  33343  aciunf1lem  33354  smatrcl  34539  smatlem  34540  qtophaus  34579  eulerpartlemgvv  35119  erdszelem10  36173  cvmlift2lem10  36285  cvmlift2lem12  36287  msubff  36503  elmpst  36509  mpstrcl  36514  elmpps  36546  dfso2  36735  fv1stcnv  36756  fv2ndcnv  36757  txpss3v  36855  dfrdg4  36930  bj-inxpALT  38176  bj-opelrelex  38188  bj-opelidres  38350  bj-elid6  38359  bj-eldiag2  38366  bj-inftyexpitaudisj  38394  curunc  38793  heiborlem3  39013  xrnss3v  39579  ecxrn2  39606  inxpxrn  39616  dibopelvalN  42466  dibopelval2  42468  dib1dim  42488  dihopcl  42576  dih1  42609  dih1dimatlem  42652  hdmap1val  43121  aks6d1c3  43439  pellex  44108  elnonrel  44847  mnringmulrcld  45487  fourierdlem42  47432  etransclem44  47561  ovn0lem  47848  ndmaovg  48527  aoprssdm  48545  ndmaovcl  48546  ndmaovrcl  48547  ndmaovcom  48548  ndmaovass  48549  ndmaovdistr  48550  sprsymrelfvlem  48845  sprsymrelfolem2  48848  prproropf1olem2  48859  opgpgvtx  49426  iinxp  50273  coxp  50275  joindm2  50413  meetdm2  50415  swapf2fval  50718  swapf1val  50720  fuco2el  50765