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 3450	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3450	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5442	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2820	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2820	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 637	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 216	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 249	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3192	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2731	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4835	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2742	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4836	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2742	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3593	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1450	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 208	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 274	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∃wrex 3069  ⟨cop 4597   × cxp 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-opab 5173  df-xp 5644

This theorem is referenced by:  opelxpi  5675  opelxp1  5679  opelxp2  5680  otelxp  5681  otel3xp  5683  brxp  5686  opthprc  5701  elxp3  5703  opeliunxp  5704  bropaex12  5728  optocl  5731  xpsspw  5770  xpiindi  5796  opelres  5948  restidsing  6011  codir  6079  qfto  6080  xpnz  6116  difxp  6121  xpdifid  6125  dfco2  6202  relssdmrnOLD  6226  ressn  6242  opelf  6708  oprab4  7448  resoprab  7479  oprssdm  7540  nssdmovg  7541  ndmovg  7542  elmpocl  7600  fo1stres  7952  fo2ndres  7953  dfoprab4  7992  opiota  7996  bropopvvv  8027  bropfvvvvlem  8028  curry1  8041  xporderlem  8064  fnwelem  8068  frpoins3xpg  8077  xpord2lem  8079  xpord2pred  8082  xpord2indlem  8084  mpoxopxprcov0  8153  mpocurryd  8205  on2recsov  8619  naddcllem  8627  brecop  8756  brecop2  8757  eceqoveq  8768  xpdom2  9018  mapunen  9097  djuss  9865  djuunxp  9866  dfac5lem2  10069  iunfo  10484  ordpipq  10887  prsrlem1  11017  opelcn  11074  opelreal  11075  elreal2  11077  swrdnznd  14542  swrd00  14544  swrdcl  14545  swrd0  14558  pfx00  14574  pfx0  14575  fsumcom2  15670  fprodcom2  15878  phimullem  16662  imasvscafn  17433  homarcl2  17935  evlfcl  18125  clatl  18411  matplusgcell  21819  iscnp2  22627  txuni2  22953  txcls  22992  txcnpi  22996  txcnp  23008  txcnmpt  23012  txdis1cn  23023  txtube  23028  hausdiag  23033  txlm  23036  tx1stc  23038  txkgen  23040  txflf  23394  tmdcn2  23477  tgphaus  23505  qustgplem  23509  fmucndlem  23680  xmeterval  23822  metustexhalf  23949  blval2  23955  bcthlem1  24725  ovolfcl  24867  ovoliunlem1  24903  mbfimaopnlem  25056  limccnp2  25293  fsumvma  26598  lgsquadlem1  26765  lgsquadlem2  26766  norec2ov  27312  dmrab  31489  xppreima2  31634  aciunf1lem  31645  f1od2  31706  smatrcl  32466  smatlem  32467  qtophaus  32506  eulerpartlemgvv  33065  erdszelem10  33881  cvmlift2lem10  33993  cvmlift2lem12  33995  msubff  34211  elmpst  34217  mpstrcl  34222  elmpps  34254  dfso2  34414  fv1stcnv  34437  fv2ndcnv  34438  txpss3v  34539  dfrdg4  34612  bj-opelrelex  35688  bj-opelidres  35705  bj-elid6  35714  bj-eldiag2  35721  bj-inftyexpitaudisj  35749  curf  36129  curunc  36133  heiborlem3  36345  xrnss3v  36907  inxpxrn  36930  dibopelvalN  39679  dibopelval2  39681  dib1dim  39701  dihopcl  39789  dih1  39822  dih1dimatlem  39865  hdmap1val  40334  pellex  41216  elnonrel  41979  mnringmulrcld  42630  fourierdlem42  44510  etransclem44  44639  ovn0lem  44926  ndmaovg  45536  aoprssdm  45554  ndmaovcl  45555  ndmaovrcl  45556  ndmaovcom  45557  ndmaovass  45558  ndmaovdistr  45559  sprsymrelfvlem  45802  sprsymrelfolem2  45805  prproropf1olem2  45816  opeliun2xp  46528  joindm2  47121  meetdm2  47123