Theorem opelxp 5303

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 5289	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3343	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3343	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5097	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2827	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2827	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 953	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 207	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 240	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3174	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2760	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4553	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2770	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4554	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2770	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3463	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1562	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 199	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 264	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 196   ∧ wa 383   = wceq 1632   ∈ wcel 2139  ∃wrex 3051  ⟨cop 4327   × cxp 5264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-opab 4865  df-xp 5272

This theorem is referenced by:  brxp  5304  opelxpi  5305  opelxp1  5307  opelxp2  5308  otel3xp  5310  opthprc  5324  elxp3  5326  opeliunxp  5327  bropaex12  5349  optocl  5352  xpsspw  5389  xpiindi  5413  opelresg  5557  opelresOLD  5561  restidsing  5616  restidsingOLD  5617  codir  5674  qfto  5675  xpnz  5711  difxp  5716  xpdifid  5720  ssrnres  5730  dfco2  5795  relssdmrn  5817  ressn  5832  elsnxpOLD  5839  opelf  6226  oprab4  6892  resoprab  6922  oprssdm  6981  nssdmovg  6982  ndmovg  6983  elmpt2cl  7042  resiexg  7268  fo1stres  7360  fo2ndres  7361  el2xptp0  7380  dfoprab4  7393  opiota  7397  bropopvvv  7424  bropfvvvvlem  7425  curry1  7438  curry2  7441  xporderlem  7457  fnwelem  7461  mpt2xopxprcov0  7513  mpt2curryd  7565  brecop  8009  brecop2  8010  eceqoveq  8021  xpdom2  8222  mapunen  8296  djuss  8957  dfac5lem2  9157  iunfo  9573  ordpipq  9976  prsrlem1  10105  opelcn  10162  opelreal  10163  elreal2  10165  swrd00  13637  swrdcl  13638  swrd0  13654  fsumcom2  14724  fsumcom2OLD  14725  fprodcom2  14933  fprodcom2OLD  14934  phimullem  15706  imasvscafn  16419  brcic  16679  homarcl2  16906  evlfcl  17083  clatl  17337  matplusgcell  20461  mdetrlin  20630  iscnp2  21265  txuni2  21590  txcls  21629  txcnpi  21633  txcnp  21645  txcnmpt  21649  txdis1cn  21660  txtube  21665  hausdiag  21670  txlm  21673  tx1stc  21675  txkgen  21677  txflf  22031  tmdcn2  22114  tgphaus  22141  qustgplem  22145  fmucndlem  22316  xmeterval  22458  metustexhalf  22582  blval2  22588  metuel2  22591  bcthlem1  23341  ovolfcl  23455  ovoliunlem1  23490  ovolshftlem1  23497  mbfimaopnlem  23641  limccnp2  23875  cxpcn3  24709  fsumvma  25158  lgsquadlem1  25325  lgsquadlem2  25326  ofresid  29774  xppreima2  29780  aciunf1lem  29792  f1od2  29829  smatrcl  30192  smatlem  30193  qtophaus  30233  eulerpartlemgvv  30768  erdszelem10  31510  cvmlift2lem10  31622  cvmlift2lem12  31624  msubff  31755  elmpst  31761  mpstrcl  31766  elmpps  31798  dfso2  31972  fv1stcnv  32006  fv2ndcnv  32007  txpss3v  32312  pprodss4v  32318  dfrdg4  32385  bj-elid3  33416  bj-eldiag2  33421  curf  33718  curunc  33722  heiborlem3  33943  opelresALTV  34373  xrnss3v  34475  inxpxrn  34494  dibopelvalN  36952  dibopelval2  36954  dib1dim  36974  dihopcl  37062  dih1  37095  dih1dimatlem  37138  hdmap1val  37608  pellex  37919  elnonrel  38411  fourierdlem42  40887  etransclem44  41016  ovn0lem  41303  ndmaovg  41788  aoprssdm  41806  ndmaovcl  41807  ndmaovrcl  41808  ndmaovcom  41809  ndmaovass  41810  ndmaovdistr  41811  pfx00  41912  pfx0  41913  sprsymrelfvlem  42268  sprsymrelfolem2  42271  opeliun2xp  42639