Theorem opelxp 5674

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 5662	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3451	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3451	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5440	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2816	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2816	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 638	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 217	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 250	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3179	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2729	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4837	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2740	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4838	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2740	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3601	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1452	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 209	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 275	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∃wrex 3053  ⟨cop 4595   × cxp 5636

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-opab 5170  df-xp 5644

This theorem is referenced by:  opelxpi  5675  opelxp1  5680  opelxp2  5681  otelxp  5682  otel3xp  5684  brxp  5687  opthprc  5702  elxp3  5704  opeliunxp  5705  opeliun2xp  5706  bropaex12  5730  optocl  5733  xpsspw  5772  inxp  5795  xpiindi  5799  opelres  5956  restidsing  6024  codir  6093  qfto  6094  xpnz  6132  difxp  6137  xpdifid  6141  dfco2  6218  relssdmrnOLD  6242  ressn  6258  opelf  6721  oprab4  7475  resoprab  7507  oprssdm  7570  nssdmovg  7571  ndmovg  7572  elmpocl  7630  fo1stres  7994  fo2ndres  7995  dfoprab4  8034  opiota  8038  bropopvvv  8069  bropfvvvvlem  8070  curry1  8083  xporderlem  8106  fnwelem  8110  frpoins3xpg  8119  xpord2lem  8121  xpord2pred  8124  xpord2indlem  8126  mpoxopxprcov0  8196  mpocurryd  8248  on2recsov  8632  naddcllem  8640  brecop  8783  brecop2  8784  eceqoveq  8795  xpdom2  9036  mapunen  9110  djuss  9873  djuunxp  9874  dfac5lem2  10077  iunfo  10492  ordpipq  10895  prsrlem1  11025  opelcn  11082  opelreal  11083  elreal2  11085  swrdnznd  14607  swrd00  14609  swrdcl  14610  swrd0  14623  pfx00  14639  pfx0  14640  fsumcom2  15740  fprodcom2  15950  phimullem  16749  imasvscafn  17500  homarcl2  17997  evlfcl  18183  clatl  18467  pzriprnglem4  21394  pzriprnglem9  21399  matplusgcell  22320  iscnp2  23126  txuni2  23452  txcls  23491  txcnpi  23495  txcnp  23507  txcnmpt  23511  txdis1cn  23522  txtube  23527  hausdiag  23532  txlm  23535  tx1stc  23537  txkgen  23539  txflf  23893  tmdcn2  23976  tgphaus  24004  qustgplem  24008  fmucndlem  24178  xmeterval  24320  metustexhalf  24444  blval2  24450  bcthlem1  25224  ovolfcl  25367  ovoliunlem1  25403  mbfimaopnlem  25556  limccnp2  25793  fsumvma  27124  lgsquadlem1  27291  lgsquadlem2  27292  norec2ov  27864  dmrab  32426  xppreima2  32575  aciunf1lem  32586  f1od2  32644  smatrcl  33786  smatlem  33787  qtophaus  33826  eulerpartlemgvv  34367  erdszelem10  35187  cvmlift2lem10  35299  cvmlift2lem12  35301  msubff  35517  elmpst  35523  mpstrcl  35528  elmpps  35560  dfso2  35742  fv1stcnv  35764  fv2ndcnv  35765  txpss3v  35866  dfrdg4  35939  bj-opelrelex  37132  bj-opelidres  37149  bj-elid6  37158  bj-eldiag2  37165  bj-inftyexpitaudisj  37193  curf  37592  curunc  37596  heiborlem3  37807  xrnss3v  38354  inxpxrn  38381  dibopelvalN  41137  dibopelval2  41139  dib1dim  41159  dihopcl  41247  dih1  41280  dih1dimatlem  41323  hdmap1val  41792  aks6d1c3  42111  pellex  42823  elnonrel  43574  mnringmulrcld  44217  fourierdlem42  46147  etransclem44  46276  ovn0lem  46563  ndmaovg  47185  aoprssdm  47203  ndmaovcl  47204  ndmaovrcl  47205  ndmaovcom  47206  ndmaovass  47207  ndmaovdistr  47208  sprsymrelfvlem  47491  sprsymrelfolem2  47494  prproropf1olem2  47505  opgpgvtx  48046  iinxp  48819  coxp  48821  joindm2  48956  meetdm2  48958  swapf2fval  49254  swapf1val  49256  fuco2el  49301