Theorem opelxp 5714

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 5702	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3465	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3465	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5482	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2813	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2813	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 636	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 216	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 249	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3189	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2725	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4875	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2736	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4876	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2736	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3619	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1446	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 208	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 274	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 205   ∧ wa 394   = wceq 1533   ∈ wcel 2098  ∃wrex 3059  ⟨cop 4636   × cxp 5676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-opab 5212  df-xp 5684

This theorem is referenced by:  opelxpi  5715  opelxp1  5720  opelxp2  5721  otelxp  5722  otel3xp  5724  brxp  5727  opthprc  5742  elxp3  5744  opeliunxp  5745  bropaex12  5769  optocl  5772  xpsspw  5811  inxp  5834  xpiindi  5838  opelres  5991  restidsing  6057  codir  6127  qfto  6128  xpnz  6165  difxp  6170  xpdifid  6174  dfco2  6251  relssdmrnOLD  6275  ressn  6291  opelf  6758  oprab4  7506  resoprab  7538  oprssdm  7602  nssdmovg  7603  ndmovg  7604  elmpocl  7662  fo1stres  8020  fo2ndres  8021  dfoprab4  8060  opiota  8064  bropopvvv  8095  bropfvvvvlem  8096  curry1  8109  xporderlem  8132  fnwelem  8136  frpoins3xpg  8145  xpord2lem  8147  xpord2pred  8150  xpord2indlem  8152  mpoxopxprcov0  8223  mpocurryd  8275  on2recsov  8689  naddcllem  8697  brecop  8829  brecop2  8830  eceqoveq  8841  xpdom2  9092  mapunen  9171  djuss  9945  djuunxp  9946  dfac5lem2  10149  iunfo  10564  ordpipq  10967  prsrlem1  11097  opelcn  11154  opelreal  11155  elreal2  11157  swrdnznd  14628  swrd00  14630  swrdcl  14631  swrd0  14644  pfx00  14660  pfx0  14661  fsumcom2  15756  fprodcom2  15964  phimullem  16751  imasvscafn  17522  homarcl2  18027  evlfcl  18217  clatl  18503  pzriprnglem4  21427  pzriprnglem9  21432  matplusgcell  22379  iscnp2  23187  txuni2  23513  txcls  23552  txcnpi  23556  txcnp  23568  txcnmpt  23572  txdis1cn  23583  txtube  23588  hausdiag  23593  txlm  23596  tx1stc  23598  txkgen  23600  txflf  23954  tmdcn2  24037  tgphaus  24065  qustgplem  24069  fmucndlem  24240  xmeterval  24382  metustexhalf  24509  blval2  24515  bcthlem1  25296  ovolfcl  25439  ovoliunlem1  25475  mbfimaopnlem  25628  limccnp2  25865  fsumvma  27191  lgsquadlem1  27358  lgsquadlem2  27359  norec2ov  27920  dmrab  32373  xppreima2  32518  aciunf1lem  32529  f1od2  32585  smatrcl  33528  smatlem  33529  qtophaus  33568  eulerpartlemgvv  34127  erdszelem10  34941  cvmlift2lem10  35053  cvmlift2lem12  35055  msubff  35271  elmpst  35277  mpstrcl  35282  elmpps  35314  dfso2  35480  fv1stcnv  35503  fv2ndcnv  35504  txpss3v  35605  dfrdg4  35678  bj-opelrelex  36754  bj-opelidres  36771  bj-elid6  36780  bj-eldiag2  36787  bj-inftyexpitaudisj  36815  curf  37202  curunc  37206  heiborlem3  37417  xrnss3v  37974  inxpxrn  37997  dibopelvalN  40746  dibopelval2  40748  dib1dim  40768  dihopcl  40856  dih1  40889  dih1dimatlem  40932  hdmap1val  41401  aks6d1c3  41726  pellex  42397  elnonrel  43157  mnringmulrcld  43807  fourierdlem42  45675  etransclem44  45804  ovn0lem  46091  ndmaovg  46702  aoprssdm  46720  ndmaovcl  46721  ndmaovrcl  46722  ndmaovcom  46723  ndmaovass  46724  ndmaovdistr  46725  sprsymrelfvlem  46967  sprsymrelfolem2  46970  prproropf1olem2  46981  opeliun2xp  47582  joindm2  48173  meetdm2  48175