Theorem opelxp 5683

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 5671	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3458	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3458	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5448	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2850	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2850	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 647	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 219	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 252	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3204	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2762	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4831	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2773	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4832	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2773	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3594	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1471	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 211	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 277	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 208   ∧ wa 399   = wceq 1560   ∈ wcel 2142  ∃wrex 3086  ⟨cop 4588   × cxp 5645

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-opab 5163  df-xp 5653

This theorem is referenced by:  opelxpi  5684  opelxp1  5689  opelxp2  5690  otelxp  5691  otel3xp  5693  brxp  5696  opthprc  5711  elxp3  5713  opeliunxp  5714  opeliun2xp  5715  bropaex12  5738  optoclOLD  5742  xpsspw  5782  inxp  5804  xpiindi  5807  opelres  5971  restidsing  6042  codir  6107  qfto  6108  xpnz  6144  difxp  6149  xpdifid  6153  xpdifcnvepel  6154  dfco2  6232  ressn  6272  opelf  6725  oprab4  7482  resoprab  7514  oprssdm  7577  nssdmovg  7578  ndmovg  7579  elmpocl  7637  fo1stres  7996  fo2ndres  7997  dfoprab4  8036  opiota  8040  bropopvvv  8069  bropfvvvvlem  8070  curry1  8083  xporderlem  8107  fnwelem  8111  frpoins3xpg  8120  xpord2lem  8122  xpord2pred  8125  xpord2indlem  8127  mpoxopxprcov0  8197  mpocurryd  8249  on2recsov  8638  naddcllem  8646  brecop  8792  brecop2  8793  eceqoveq  8804  xpdom2  9044  mapunen  9118  djuss  9878  djuunxp  9879  dfac5lem2  10080  iunfo  10496  ordpipq  10900  prsrlem1  11030  opelcn  11087  opelreal  11088  elreal2  11090  swrdnznd  14656  swrd00  14658  swrdcl  14659  swrd0  14672  pfx00  14688  pfx0  14689  fsumcom2  15801  fprodcom2  16014  phimullem  16814  imasvscafn  17567  homarcl2  18068  evlfcl  18254  clatl  18540  pzriprnglem4  21536  pzriprnglem9  21541  matplusgcell  22493  iscnp2  23299  txuni2  23625  txcls  23664  txcnpi  23668  txcnp  23680  txcnmpt  23684  txdis1cn  23695  txtube  23700  hausdiag  23705  txlm  23708  tx1stc  23710  txkgen  23712  txflf  24066  tmdcn2  24149  tgphaus  24177  qustgplem  24181  fmucndlem  24350  xmeterval  24492  metustexhalf  24616  blval2  24622  bcthlem1  25386  ovolfcl  25528  ovoliunlem1  25564  mbfimaopnlem  25717  limccnp2  25954  fsumvma  27277  lgsquadlem1  27444  lgsquadlem2  27445  norec2ov  28050  dmrab  32696  xppreima2  32853  aciunf1lem  32864  f1od2  32921  smatrcl  34093  smatlem  34094  qtophaus  34133  eulerpartlemgvv  34673  erdszelem10  35550  cvmlift2lem10  35662  cvmlift2lem12  35664  msubff  35880  elmpst  35886  mpstrcl  35891  elmpps  35923  dfso2  36105  fv1stcnv  36127  fv2ndcnv  36128  txpss3v  36226  dfrdg4  36301  bj-opelrelex  37636  bj-opelidres  37653  bj-elid6  37662  bj-eldiag2  37669  bj-inftyexpitaudisj  37697  curf  38097  curunc  38101  heiborlem3  38312  xrnss3v  38880  ecxrn2  38907  inxpxrn  38917  dibopelvalN  41767  dibopelval2  41769  dib1dim  41789  dihopcl  41877  dih1  41910  dih1dimatlem  41953  hdmap1val  42422  aks6d1c3  42740  pellex  43412  elnonrel  44161  mnringmulrcld  44804  fourierdlem42  46723  etransclem44  46852  ovn0lem  47139  ndmaovg  47778  aoprssdm  47796  ndmaovcl  47797  ndmaovrcl  47798  ndmaovcom  47799  ndmaovass  47800  ndmaovdistr  47801  sprsymrelfvlem  48096  sprsymrelfolem2  48099  prproropf1olem2  48110  opgpgvtx  48677  iinxp  49452  coxp  49454  joindm2  49589  meetdm2  49591  swapf2fval  49886  swapf1val  49888  fuco2el  49933