Theorem opelxp 5626

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 5614	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3437	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3437	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5396	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2827	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2827	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 636	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 216	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 249	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3222	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2739	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4805	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2750	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4806	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2750	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3573	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1449	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 208	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 274	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2107  ∃wrex 3066  ⟨cop 4568   × cxp 5588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-opab 5138  df-xp 5596

This theorem is referenced by:  opelxpi  5627  opelxp1  5631  opelxp2  5632  otel3xp  5634  brxp  5637  opthprc  5652  elxp3  5654  opeliunxp  5655  bropaex12  5679  optocl  5682  xpsspw  5721  xpiindi  5747  opelres  5900  restidsing  5965  codir  6030  qfto  6031  xpnz  6067  difxp  6072  xpdifid  6076  dfco2  6153  relssdmrn  6176  ressn  6192  opelf  6644  oprab4  7370  resoprab  7401  oprssdm  7462  nssdmovg  7463  ndmovg  7464  elmpocl  7520  fo1stres  7866  fo2ndres  7867  dfoprab4  7904  opiota  7908  bropopvvv  7939  bropfvvvvlem  7940  curry1  7953  xporderlem  7977  fnwelem  7981  mpoxopxprcov0  8042  mpocurryd  8094  brecop  8608  brecop2  8609  eceqoveq  8620  xpdom2  8863  mapunen  8942  djuss  9687  djuunxp  9688  dfac5lem2  9889  iunfo  10304  ordpipq  10707  prsrlem1  10837  opelcn  10894  opelreal  10895  elreal2  10897  swrdnznd  14364  swrd00  14366  swrdcl  14367  swrd0  14380  pfx00  14396  pfx0  14397  fsumcom2  15495  fprodcom2  15703  phimullem  16489  imasvscafn  17257  homarcl2  17759  evlfcl  17949  clatl  18235  matplusgcell  21591  iscnp2  22399  txuni2  22725  txcls  22764  txcnpi  22768  txcnp  22780  txcnmpt  22784  txdis1cn  22795  txtube  22800  hausdiag  22805  txlm  22808  tx1stc  22810  txkgen  22812  txflf  23166  tmdcn2  23249  tgphaus  23277  qustgplem  23281  fmucndlem  23452  xmeterval  23594  metustexhalf  23721  blval2  23727  bcthlem1  24497  ovolfcl  24639  ovoliunlem1  24675  mbfimaopnlem  24828  limccnp2  25065  fsumvma  26370  lgsquadlem1  26537  lgsquadlem2  26538  dmrab  30853  xppreima2  30997  aciunf1lem  31008  f1od2  31065  smatrcl  31755  smatlem  31756  qtophaus  31795  eulerpartlemgvv  32352  erdszelem10  33171  cvmlift2lem10  33283  cvmlift2lem12  33285  msubff  33501  elmpst  33507  mpstrcl  33512  elmpps  33544  ot2elxp  33688  dfso2  33731  fv1stcnv  33760  fv2ndcnv  33761  frpoins3xpg  33796  xpord2lem  33798  xpord2pred  33801  xpord2ind  33803  xpord3pred  33807  on2recsov  33836  naddcllem  33840  norec2ov  34123  txpss3v  34189  dfrdg4  34262  bj-opelrelex  35324  bj-opelidres  35341  bj-elid6  35350  bj-eldiag2  35357  bj-inftyexpitaudisj  35385  curf  35764  curunc  35768  heiborlem3  35980  xrnss3v  36509  inxpxrn  36528  dibopelvalN  39164  dibopelval2  39166  dib1dim  39186  dihopcl  39274  dih1  39307  dih1dimatlem  39350  hdmap1val  39819  pellex  40664  elnonrel  41200  mnringmulrcld  41853  fourierdlem42  43697  etransclem44  43826  ovn0lem  44110  ndmaovg  44687  aoprssdm  44705  ndmaovcl  44706  ndmaovrcl  44707  ndmaovcom  44708  ndmaovass  44709  ndmaovdistr  44710  sprsymrelfvlem  44953  sprsymrelfolem2  44956  prproropf1olem2  44967  opeliun2xp  45679  joindm2  46273  meetdm2  46275