Theorem opelxp 5616

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 5604	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3426	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3426	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5389	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2826	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2826	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 635	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 216	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 249	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3220	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2738	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4801	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2749	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4802	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2749	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3564	. . . 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 1539   ∈ wcel 2108  ∃wrex 3064  ⟨cop 4564   × cxp 5578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-opab 5133  df-xp 5586

This theorem is referenced by:  opelxpi  5617  opelxp1  5621  opelxp2  5622  otel3xp  5624  brxp  5627  opthprc  5642  elxp3  5644  opeliunxp  5645  bropaex12  5668  optocl  5671  xpsspw  5708  xpiindi  5733  opelres  5886  restidsing  5951  codir  6014  qfto  6015  xpnz  6051  difxp  6056  xpdifid  6060  dfco2  6138  relssdmrn  6161  ressn  6177  opelf  6619  oprab4  7339  resoprab  7370  oprssdm  7431  nssdmovg  7432  ndmovg  7433  elmpocl  7489  fo1stres  7830  fo2ndres  7831  dfoprab4  7868  opiota  7872  bropopvvv  7901  bropfvvvvlem  7902  curry1  7915  xporderlem  7939  fnwelem  7943  mpoxopxprcov0  8004  mpocurryd  8056  brecop  8557  brecop2  8558  eceqoveq  8569  xpdom2  8807  mapunen  8882  djuss  9609  djuunxp  9610  dfac5lem2  9811  iunfo  10226  ordpipq  10629  prsrlem1  10759  opelcn  10816  opelreal  10817  elreal2  10819  swrdnznd  14283  swrd00  14285  swrdcl  14286  swrd0  14299  pfx00  14315  pfx0  14316  fsumcom2  15414  fprodcom2  15622  phimullem  16408  imasvscafn  17165  homarcl2  17666  evlfcl  17856  clatl  18141  matplusgcell  21490  iscnp2  22298  txuni2  22624  txcls  22663  txcnpi  22667  txcnp  22679  txcnmpt  22683  txdis1cn  22694  txtube  22699  hausdiag  22704  txlm  22707  tx1stc  22709  txkgen  22711  txflf  23065  tmdcn2  23148  tgphaus  23176  qustgplem  23180  fmucndlem  23351  xmeterval  23493  metustexhalf  23618  blval2  23624  bcthlem1  24393  ovolfcl  24535  ovoliunlem1  24571  mbfimaopnlem  24724  limccnp2  24961  fsumvma  26266  lgsquadlem1  26433  lgsquadlem2  26434  dmrab  30745  xppreima2  30889  aciunf1lem  30901  f1od2  30958  smatrcl  31648  smatlem  31649  qtophaus  31688  eulerpartlemgvv  32243  erdszelem10  33062  cvmlift2lem10  33174  cvmlift2lem12  33176  msubff  33392  elmpst  33398  mpstrcl  33403  elmpps  33435  ot2elxp  33582  dfso2  33628  fv1stcnv  33657  fv2ndcnv  33658  frpoins3xpg  33714  xpord2lem  33716  xpord2pred  33719  xpord2ind  33721  xpord3pred  33725  on2recsov  33754  naddcllem  33758  norec2ov  34041  txpss3v  34107  dfrdg4  34180  bj-opelrelex  35242  bj-opelidres  35259  bj-elid6  35268  bj-eldiag2  35275  bj-inftyexpitaudisj  35303  curf  35682  curunc  35686  heiborlem3  35898  xrnss3v  36429  inxpxrn  36448  dibopelvalN  39084  dibopelval2  39086  dib1dim  39106  dihopcl  39194  dih1  39227  dih1dimatlem  39270  hdmap1val  39739  pellex  40573  elnonrel  41082  mnringmulrcld  41735  fourierdlem42  43580  etransclem44  43709  ovn0lem  43993  ndmaovg  44563  aoprssdm  44581  ndmaovcl  44582  ndmaovrcl  44583  ndmaovcom  44584  ndmaovass  44585  ndmaovdistr  44586  sprsymrelfvlem  44830  sprsymrelfolem2  44833  prproropf1olem2  44844  opeliun2xp  45556  joindm2  46150  meetdm2  46152