Theorem opelxp 5594

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 5582	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3500	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3500	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5375	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2903	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2903	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 637	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 219	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 252	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3295	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2824	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4806	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2835	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4807	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2835	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3638	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1446	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 211	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 277	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1536   ∈ wcel 2113  ∃wrex 3142  ⟨cop 4576   × cxp 5556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pr 5333

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-opab 5132  df-xp 5564

This theorem is referenced by:  opelxpi  5595  opelxp1  5599  opelxp2  5600  otel3xp  5602  brxp  5604  opthprc  5619  elxp3  5621  opeliunxp  5622  bropaex12  5645  optocl  5648  xpsspw  5685  xpiindi  5709  opelres  5862  restidsing  5925  codir  5983  qfto  5984  xpnz  6019  difxp  6024  xpdifid  6028  dfco2  6101  relssdmrn  6124  ressn  6139  opelf  6542  oprab4  7243  resoprab  7273  oprssdm  7332  nssdmovg  7333  ndmovg  7334  elmpocl  7390  fo1stres  7718  fo2ndres  7719  dfoprab4  7756  opiota  7760  bropopvvv  7788  bropfvvvvlem  7789  curry1  7802  xporderlem  7824  fnwelem  7828  mpoxopxprcov0  7886  mpocurryd  7938  brecop  8393  brecop2  8394  eceqoveq  8405  xpdom2  8615  mapunen  8689  djuss  9352  djuunxp  9353  dfac5lem2  9553  iunfo  9964  ordpipq  10367  prsrlem1  10497  opelcn  10554  opelreal  10555  elreal2  10557  swrdnznd  14007  swrd00  14009  swrdcl  14010  swrd0  14023  pfx00  14039  pfx0  14040  fsumcom2  15132  fprodcom2  15341  phimullem  16119  imasvscafn  16813  homarcl2  17298  evlfcl  17475  clatl  17729  matplusgcell  21045  iscnp2  21850  txuni2  22176  txcls  22215  txcnpi  22219  txcnp  22231  txcnmpt  22235  txdis1cn  22246  txtube  22251  hausdiag  22256  txlm  22259  tx1stc  22261  txkgen  22263  txflf  22617  tmdcn2  22700  tgphaus  22728  qustgplem  22732  fmucndlem  22903  xmeterval  23045  metustexhalf  23169  blval2  23175  bcthlem1  23930  ovolfcl  24070  ovoliunlem1  24106  mbfimaopnlem  24259  limccnp2  24493  fsumvma  25792  lgsquadlem1  25959  lgsquadlem2  25960  dmrab  30263  xppreima2  30398  aciunf1lem  30410  f1od2  30460  smatrcl  31065  smatlem  31066  qtophaus  31104  eulerpartlemgvv  31638  erdszelem10  32451  cvmlift2lem10  32563  cvmlift2lem12  32565  msubff  32781  elmpst  32787  mpstrcl  32792  elmpps  32824  dfso2  32994  fv1stcnv  33024  fv2ndcnv  33025  txpss3v  33343  dfrdg4  33416  bj-opelrelex  34440  bj-opelidres  34457  bj-elid6  34466  bj-eldiag2  34473  bj-inftyexpitaudisj  34491  curf  34874  curunc  34878  heiborlem3  35095  xrnss3v  35628  inxpxrn  35647  dibopelvalN  38283  dibopelval2  38285  dib1dim  38305  dihopcl  38393  dih1  38426  dih1dimatlem  38469  hdmap1val  38938  pellex  39438  elnonrel  39951  fourierdlem42  42441  etransclem44  42570  ovn0lem  42854  ndmaovg  43390  aoprssdm  43408  ndmaovcl  43409  ndmaovrcl  43410  ndmaovcom  43411  ndmaovass  43412  ndmaovdistr  43413  sprsymrelfvlem  43659  sprsymrelfolem2  43662  prproropf1olem2  43673  opeliun2xp  44388