Theorem opelxp 5106

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 5092	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3189	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3189	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 4909	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2686	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2686	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 916	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 207	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 240	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3029	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2621	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4370	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2631	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4371	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2631	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3308	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1410	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 199	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 264	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 196   ∧ wa 384   = wceq 1480   ∈ wcel 1987  ∃wrex 2908  ⟨cop 4154   × cxp 5072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pr 4867

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-opab 4674  df-xp 5080

This theorem is referenced by:  brxp  5107  opelxpi  5108  opelxp1  5110  opelxp2  5111  otel3xp  5113  opthprc  5127  elxp3  5130  opeliunxp  5131  bropaex12  5153  optocl  5156  xpsspw  5194  xpiindi  5217  opelres  5361  restidsing  5417  restidsingOLD  5418  codir  5475  qfto  5476  xpnz  5512  difxp  5517  xpdifid  5521  ssrnres  5531  dfco2  5593  relssdmrn  5615  ressn  5630  elsnxpOLD  5637  opelf  6022  oprab4  6679  resoprab  6709  oprssdm  6768  nssdmovg  6769  ndmovg  6770  elmpt2cl  6829  resiexg  7049  fo1stres  7137  fo2ndres  7138  el2xptp0  7157  dfoprab4  7170  opiota  7174  bropopvvv  7200  bropfvvvvlem  7201  curry1  7214  curry2  7217  xporderlem  7233  fnwelem  7237  mpt2xopxprcov0  7288  mpt2curryd  7340  brecop  7785  brecop2  7786  eceqoveq  7798  xpdom2  7999  mapunen  8073  dfac5lem2  8891  iunfo  9305  ordpipq  9708  prsrlem1  9837  opelcn  9894  opelreal  9895  elreal2  9897  swrd00  13356  swrdcl  13357  swrd0  13372  fsumcom2  14433  fsumcom2OLD  14434  fprodcom2  14639  fprodcom2OLD  14640  phimullem  15408  imasvscafn  16118  brcic  16379  homarcl2  16606  evlfcl  16783  clatl  17037  matplusgcell  20158  mdetrlin  20327  iscnp2  20953  txuni2  21278  txcls  21317  txcnpi  21321  txcnp  21333  txcnmpt  21337  txdis1cn  21348  txtube  21353  hausdiag  21358  txlm  21361  tx1stc  21363  txkgen  21365  txflf  21720  tmdcn2  21803  tgphaus  21830  qustgplem  21834  fmucndlem  22005  xmeterval  22147  metustexhalf  22271  blval2  22277  metuel2  22280  bcthlem1  23029  ovolfcl  23142  ovoliunlem1  23177  ovolshftlem1  23184  mbfimaopnlem  23328  limccnp2  23562  cxpcn3  24389  fsumvma  24838  lgsquadlem1  25005  lgsquadlem2  25006  ofresid  29283  xppreima2  29289  aciunf1lem  29301  f1od2  29339  smatrcl  29641  smatlem  29642  qtophaus  29682  eulerpartlemgvv  30216  erdszelem10  30887  cvmlift2lem10  30999  cvmlift2lem12  31001  msubff  31132  elmpst  31138  mpstrcl  31143  elmpps  31175  dfso2  31349  fv1stcnv  31379  fv2ndcnv  31380  txpss3v  31624  pprodss4v  31630  dfrdg4  31697  bj-elid3  32717  bj-eldiag2  32722  curf  33016  curunc  33020  heiborlem3  33241  dibopelvalN  35909  dibopelval2  35911  dib1dim  35931  dihopcl  36019  dih1  36052  dih1dimatlem  36095  hdmap1val  36565  pellex  36876  elnonrel  37369  fourierdlem42  39670  etransclem44  39799  ovn0lem  40083  ndmaovg  40565  aoprssdm  40583  ndmaovcl  40584  ndmaovrcl  40585  ndmaovcom  40586  ndmaovass  40587  ndmaovdistr  40588  pfx00  40680  pfx0  40681  sprsymrelfvlem  41025  sprsymrelfolem2  41028  opeliun2xp  41396