Theorem opelxpd 5660

Description: Ordered pair membership in a Cartesian product, deduction form. (Contributed by Glauco Siliprandi, 3-Mar-2021.)

Hypotheses

Ref	Expression
opelxpd.1	⊢ (𝜑 → 𝐴 ∈ 𝐶)
opelxpd.2	⊢ (𝜑 → 𝐵 ∈ 𝐷)

Assertion

Ref	Expression
opelxpd	⊢ (𝜑 → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Proof of Theorem opelxpd

Step	Hyp	Ref	Expression
1		opelxpd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐶)
2		opelxpd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐷)
3		opelxpi 5658	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
4	1, 2, 3	syl2anc 591	1 ⊢ (𝜑 → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Syntax hints:   → wi 4   ∈ wcel 2121  ⟨cop 4564   × cxp 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221  ax-pr 5365

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-opab 5138  df-xp 5627

This theorem is referenced by:  otel3xp  5667  opabssxpd  5668  relssdmrn  6224  fpr2g  7159  fliftrel  7256  elovimad  7410  el2xptp0  7982  oprab2co  8040  1stconst  8043  2ndconst  8044  curry2  8050  fsplitfpar  8061  offsplitfpar  8062  mpof1o2d  8069  fnwelem  8075  xpf1o  9071  xpmapenlem  9076  unxpdomlem3  9162  fseqenlem1  9941  fseqenlem2  9942  iundom2g  10457  ordpipq  10860  addpqf  10862  mulpqf  10864  recmulnq  10882  ltexnq  10893  axmulf  11064  cnrecnv  15122  ruclem1  16193  eucalgf  16547  qredeu  16622  crth  16743  phimullem  16744  prmreclem3  16884  setsstruct2  17139  imasaddflem  17489  xpsaddlem  17532  xpsvsca  17536  xpsle  17538  comffval  17660  oppccofval  17677  isoval  17727  brcic  17760  funcf2  17830  idfu2nd  17839  resf2nd  17857  wunfunc  17863  homaval  17993  setcco  18045  catcco  18067  estrcco  18091  xpcco  18144  xpchom2  18147  xpcco2  18148  xpccatid  18149  prfcl  18164  prf1st  18165  prf2nd  18166  evlf2  18179  curf1cl  18189  curf2cl  18192  curfcl  18193  uncf1  18197  uncf2  18198  uncfcurf  18200  diag11  18204  diag12  18205  diag2  18206  curf2ndf  18208  hof2fval  18216  yonedalem21  18234  yonedalem22  18239  yonedalem3b  18240  yonffthlem  18243  latcl2  18397  xpsmnd0  18741  xpsinv  19031  xpsgrpsub  19032  lsmhash  19675  frgpuplem  19742  xpsring1d  20308  rngqiprngimf  21294  pzriprnglem4  21463  pzriprnglem5  21464  pzriprnglem8  21467  pzriprnglem12  21471  mdetrlin  22589  mdetrsca  22590  txcls  23591  txcnp  23607  txcnmpt  23611  txdis1cn  23622  txlly  23623  txnlly  23624  txlm  23635  lmcn2  23636  txkgen  23639  xkococnlem  23646  txhmeo  23790  ptuncnv  23794  txflf  23993  flfcnp2  23994  tmdcn2  24076  qustgplem  24108  tsmsadd  24134  imasdsf1olem  24360  xpsdsval  24368  comet  24500  metustid  24541  metustexhalf  24543  metuel2  24552  tngnm  24638  cnheiborlem  24943  bcthlem5  25317  ovollb2lem  25477  ovolctb  25479  ovoliunlem2  25492  ovolshftlem1  25498  ovolscalem1  25502  ovolicc1  25505  ioombl1lem1  25547  dyadf  25580  itg1addlem4  25688  limccnp2  25881  dvaddbr  25927  dvmulbr  25928  dvcobr  25935  lhop1lem  26002  cxpcn3  26734  mpodvdsmulf1o  27179  dvdsmulf1o  27181  addsqnreup  27428  addsval  27976  mulsval  28123  tgjustc1  28565  tgjustc2  28566  tgelrnln  28720  numclwwlk1lem2f  30447  ofresid  32738  fsuppcurry1  32820  fsuppcurry2  32821  gsumpart  33148  gsumwrd2dccatlem  33162  gsumwrd2dccat  33163  elrgspnsubrunlem2  33333  erlbrd  33348  rlocaddval  33353  rlocmulval  33354  rloccring  33355  rloc0g  33356  rloc1r  33357  rlocf1  33358  fracerl  33394  fracfld  33396  zringfrac  33649  prsdm  34110  prsrn  34111  esum2dlem  34288  hgt750lemb  34852  cvmlift2lem10  35555  goelel3xp  35591  sat1el2xp  35622  fmla0xp  35626  prv1n  35674  pprodss4v  36125  poimirlem3  38005  poimirlem4  38006  poimirlem17  38019  poimirlem20  38022  mblfinlem2  38040  aks6d1c3  42623  aks6d1c7lem1  42680  projf1o  45657  hoicvr  47005  ovolval4lem1  47106  ovolval5lem2  47110  gpgiedgdmellem  48551  gpgvtx0  48558  gpgvtx1  48559  gpg3kgrtriex  48594  gpgprismgr4cycllem3  48602  gpgprismgr4cycllem9  48608  tposidres  49390  oppf1st2nd  49635  imaid  49658  xpcfuccocl  49761  swapf1  49776  swapf2val  49777  swapf2  49778  cofuswapf1  49798  cofuswapf2  49799  lanfval  50117  ranfval  50118