Theorem opelxp 5444

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 5432	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3418	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3418	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5230	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2853	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2853	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 626	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 209	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 242	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3237	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2778	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4678	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2788	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4679	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2788	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3550	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1429	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 201	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 267	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 198   ∧ wa 387   = wceq 1507   ∈ wcel 2050  ∃wrex 3089  ⟨cop 4448   × cxp 5406

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750  ax-sep 5061  ax-nul 5068  ax-pr 5187

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4181  df-if 4352  df-sn 4443  df-pr 4445  df-op 4449  df-opab 4993  df-xp 5414

This theorem is referenced by:  opelxpi  5445  opelxp1  5449  opelxp2  5450  otel3xp  5452  brxp  5454  opthprc  5467  elxp3  5469  opeliunxp  5470  bropaex12  5493  optocl  5496  xpsspw  5533  xpiindi  5557  opelres  5702  opelresgOLD2  5706  restidsing  5766  codir  5822  qfto  5823  xpnz  5858  difxp  5863  xpdifid  5867  dfco2  5939  relssdmrn  5961  ressn  5976  opelf  6370  oprab4  7058  resoprab  7088  oprssdm  7147  nssdmovg  7148  ndmovg  7149  elmpocl  7208  fo1stres  7529  fo2ndres  7530  dfoprab4  7563  opiota  7567  bropopvvv  7595  bropfvvvvlem  7596  curry1  7609  xporderlem  7628  fnwelem  7632  mpoxopxprcov0  7688  mpocurryd  7740  brecop  8192  brecop2  8193  eceqoveq  8204  xpdom2  8410  mapunen  8484  djuss  9145  djuunxp  9146  dfac5lem2  9346  iunfo  9761  ordpipq  10164  prsrlem1  10294  opelcn  10351  opelreal  10352  elreal2  10354  swrdnznd  13808  swrd00  13810  swrdcl  13811  swrd0  13829  pfx00  13859  pfx0  13860  fsumcom2  14992  fprodcom2  15201  phimullem  15975  imasvscafn  16669  homarcl2  17156  evlfcl  17333  clatl  17587  matplusgcell  20749  iscnp2  21554  txuni2  21880  txcls  21919  txcnpi  21923  txcnp  21935  txcnmpt  21939  txdis1cn  21950  txtube  21955  hausdiag  21960  txlm  21963  tx1stc  21965  txkgen  21967  txflf  22321  tmdcn2  22404  tgphaus  22431  qustgplem  22435  fmucndlem  22606  xmeterval  22748  metustexhalf  22872  blval2  22878  bcthlem1  23633  ovolfcl  23773  ovoliunlem1  23809  mbfimaopnlem  23962  limccnp2  24196  fsumvma  25494  lgsquadlem1  25661  lgsquadlem2  25662  dmrab  30042  xppreima2  30160  aciunf1lem  30172  f1od2  30212  smatrcl  30703  smatlem  30704  qtophaus  30744  eulerpartlemgvv  31279  erdszelem10  32032  cvmlift2lem10  32144  cvmlift2lem12  32146  msubff  32297  elmpst  32303  mpstrcl  32308  elmpps  32340  dfso2  32510  fv1stcnv  32540  fv2ndcnv  32541  txpss3v  32860  dfrdg4  32933  bj-elid3  33940  bj-eldiag2  33946  bj-inftyexpitaudisj  33956  curf  34311  curunc  34315  heiborlem3  34533  xrnss3v  35069  inxpxrn  35088  dibopelvalN  37724  dibopelval2  37726  dib1dim  37746  dihopcl  37834  dih1  37867  dih1dimatlem  37910  hdmap1val  38379  pellex  38828  elnonrel  39307  fourierdlem42  41866  etransclem44  41995  ovn0lem  42279  ndmaovg  42790  aoprssdm  42808  ndmaovcl  42809  ndmaovrcl  42810  ndmaovcom  42811  ndmaovass  42812  ndmaovdistr  42813  sprsymrelfvlem  43021  sprsymrelfolem2  43024  prproropf1olem2  43035  opeliun2xp  43746