Theorem opelxp 5624

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 5612	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3434	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3434	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5397	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2827	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2827	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 635	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 216	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 249	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3222	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2739	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4809	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2750	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4810	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2750	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3572	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1448	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 208	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 274	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 205   ∧ wa 395   = wceq 1541   ∈ wcel 2109  ∃wrex 3066  ⟨cop 4572   × cxp 5586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-opab 5141  df-xp 5594

This theorem is referenced by:  opelxpi  5625  opelxp1  5629  opelxp2  5630  otel3xp  5632  brxp  5635  opthprc  5650  elxp3  5652  opeliunxp  5653  bropaex12  5676  optocl  5679  xpsspw  5716  xpiindi  5741  opelres  5894  restidsing  5959  codir  6022  qfto  6023  xpnz  6059  difxp  6064  xpdifid  6068  dfco2  6146  relssdmrn  6169  ressn  6185  opelf  6631  oprab4  7352  resoprab  7383  oprssdm  7444  nssdmovg  7445  ndmovg  7446  elmpocl  7502  fo1stres  7843  fo2ndres  7844  dfoprab4  7881  opiota  7885  bropopvvv  7914  bropfvvvvlem  7915  curry1  7928  xporderlem  7952  fnwelem  7956  mpoxopxprcov0  8017  mpocurryd  8069  brecop  8573  brecop2  8574  eceqoveq  8585  xpdom2  8823  mapunen  8898  djuss  9662  djuunxp  9663  dfac5lem2  9864  iunfo  10279  ordpipq  10682  prsrlem1  10812  opelcn  10869  opelreal  10870  elreal2  10872  swrdnznd  14336  swrd00  14338  swrdcl  14339  swrd0  14352  pfx00  14368  pfx0  14369  fsumcom2  15467  fprodcom2  15675  phimullem  16461  imasvscafn  17229  homarcl2  17731  evlfcl  17921  clatl  18207  matplusgcell  21563  iscnp2  22371  txuni2  22697  txcls  22736  txcnpi  22740  txcnp  22752  txcnmpt  22756  txdis1cn  22767  txtube  22772  hausdiag  22777  txlm  22780  tx1stc  22782  txkgen  22784  txflf  23138  tmdcn2  23221  tgphaus  23249  qustgplem  23253  fmucndlem  23424  xmeterval  23566  metustexhalf  23693  blval2  23699  bcthlem1  24469  ovolfcl  24611  ovoliunlem1  24647  mbfimaopnlem  24800  limccnp2  25037  fsumvma  26342  lgsquadlem1  26509  lgsquadlem2  26510  dmrab  30823  xppreima2  30967  aciunf1lem  30978  f1od2  31035  smatrcl  31725  smatlem  31726  qtophaus  31765  eulerpartlemgvv  32322  erdszelem10  33141  cvmlift2lem10  33253  cvmlift2lem12  33255  msubff  33471  elmpst  33477  mpstrcl  33482  elmpps  33514  ot2elxp  33658  dfso2  33701  fv1stcnv  33730  fv2ndcnv  33731  frpoins3xpg  33766  xpord2lem  33768  xpord2pred  33771  xpord2ind  33773  xpord3pred  33777  on2recsov  33806  naddcllem  33810  norec2ov  34093  txpss3v  34159  dfrdg4  34232  bj-opelrelex  35294  bj-opelidres  35311  bj-elid6  35320  bj-eldiag2  35327  bj-inftyexpitaudisj  35355  curf  35734  curunc  35738  heiborlem3  35950  xrnss3v  36481  inxpxrn  36500  dibopelvalN  39136  dibopelval2  39138  dib1dim  39158  dihopcl  39246  dih1  39279  dih1dimatlem  39322  hdmap1val  39791  pellex  40637  elnonrel  41146  mnringmulrcld  41799  fourierdlem42  43644  etransclem44  43773  ovn0lem  44057  ndmaovg  44627  aoprssdm  44645  ndmaovcl  44646  ndmaovrcl  44647  ndmaovcom  44648  ndmaovass  44649  ndmaovdistr  44650  sprsymrelfvlem  44894  sprsymrelfolem2  44897  prproropf1olem2  44908  opeliun2xp  45620  joindm2  46214  meetdm2  46216