Theorem opelxpd 5659

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 5657	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Syntax hints:   → wi 4   ∈ wcel 2114  ⟨cop 4563   × cxp 5618

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707  ax-sep 5220  ax-pr 5364

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-opab 5137  df-xp 5626

This theorem is referenced by:  otel3xp  5666  opabssxpd  5667  relssdmrn  6222  fpr2g  7155  fliftrel  7252  elovimad  7406  el2xptp0  7978  oprab2co  8036  1stconst  8039  2ndconst  8040  curry2  8046  fsplitfpar  8057  offsplitfpar  8058  fnwelem  8070  xpf1o  9066  xpmapenlem  9071  unxpdomlem3  9157  fseqenlem1  9935  fseqenlem2  9936  iundom2g  10451  ordpipq  10854  addpqf  10856  mulpqf  10858  recmulnq  10876  ltexnq  10887  axmulf  11058  cnrecnv  15116  ruclem1  16187  eucalgf  16541  qredeu  16616  crth  16737  phimullem  16738  prmreclem3  16878  setsstruct2  17133  imasaddflem  17483  xpsaddlem  17526  xpsvsca  17530  xpsle  17532  comffval  17654  oppccofval  17671  isoval  17721  brcic  17754  funcf2  17824  idfu2nd  17833  resf2nd  17851  wunfunc  17857  homaval  17987  setcco  18039  catcco  18061  estrcco  18085  xpcco  18138  xpchom2  18141  xpcco2  18142  xpccatid  18143  prfcl  18158  prf1st  18159  prf2nd  18160  evlf2  18173  curf1cl  18183  curf2cl  18186  curfcl  18187  uncf1  18191  uncf2  18192  uncfcurf  18194  diag11  18198  diag12  18199  diag2  18200  curf2ndf  18202  hof2fval  18210  yonedalem21  18228  yonedalem22  18233  yonedalem3b  18234  yonffthlem  18237  latcl2  18391  xpsmnd0  18735  xpsinv  19025  xpsgrpsub  19026  lsmhash  19669  frgpuplem  19736  xpsring1d  20302  rngqiprngimf  21284  pzriprnglem4  21453  pzriprnglem5  21454  pzriprnglem8  21457  pzriprnglem12  21461  mdetrlin  22555  mdetrsca  22556  txcls  23557  txcnp  23573  txcnmpt  23577  txdis1cn  23588  txlly  23589  txnlly  23590  txlm  23601  lmcn2  23602  txkgen  23605  xkococnlem  23612  txhmeo  23756  ptuncnv  23760  txflf  23959  flfcnp2  23960  tmdcn2  24042  qustgplem  24074  tsmsadd  24100  imasdsf1olem  24326  xpsdsval  24334  comet  24466  metustid  24507  metustexhalf  24509  metuel2  24518  tngnm  24604  cnheiborlem  24909  bcthlem5  25283  ovollb2lem  25443  ovolctb  25445  ovoliunlem2  25458  ovolshftlem1  25464  ovolscalem1  25468  ovolicc1  25471  ioombl1lem1  25513  dyadf  25546  itg1addlem4  25654  limccnp2  25847  dvaddbr  25893  dvmulbr  25894  dvcobr  25901  lhop1lem  25968  cxpcn3  26700  mpodvdsmulf1o  27145  dvdsmulf1o  27147  addsqnreup  27394  addsval  27942  mulsval  28089  tgjustc1  28531  tgjustc2  28532  tgelrnln  28686  numclwwlk1lem2f  30413  ofresid  32703  fsuppcurry1  32785  fsuppcurry2  32786  gsumpart  33112  gsumwrd2dccatlem  33126  gsumwrd2dccat  33127  elrgspnsubrunlem2  33297  erlbrd  33312  rlocaddval  33317  rlocmulval  33318  rloccring  33319  rloc0g  33320  rloc1r  33321  rlocf1  33322  fracerl  33355  fracfld  33357  zringfrac  33602  prsdm  34046  prsrn  34047  esum2dlem  34224  hgt750lemb  34788  cvmlift2lem10  35482  goelel3xp  35518  sat1el2xp  35549  fmla0xp  35553  prv1n  35601  pprodss4v  36052  poimirlem3  37932  poimirlem4  37933  poimirlem17  37946  poimirlem20  37949  mblfinlem2  37967  aks6d1c3  42550  aks6d1c7lem1  42607  f1o2d2  42662  projf1o  45614  hoicvr  46964  ovolval4lem1  47065  ovolval5lem2  47069  gpgiedgdmellem  48510  gpgvtx0  48517  gpgvtx1  48518  gpg3kgrtriex  48553  gpgprismgr4cycllem3  48561  gpgprismgr4cycllem9  48567  tposidres  49349  oppf1st2nd  49594  imaid  49617  xpcfuccocl  49720  swapf1  49735  swapf2val  49736  swapf2  49737  cofuswapf1  49757  cofuswapf2  49758  lanfval  50076  ranfval  50077