Theorem opelxpd 5664

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

Syntax hints:   → wi 4   ∈ wcel 2114  ⟨cop 4587   × cxp 5623

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 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378

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 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-opab 5162  df-xp 5631

This theorem is referenced by:  otel3xp  5671  opabssxpd  5672  relssdmrn  6228  fpr2g  7159  fliftrel  7256  elovimad  7410  el2xptp0  7982  oprab2co  8041  1stconst  8044  2ndconst  8045  curry2  8051  fsplitfpar  8062  offsplitfpar  8063  fnwelem  8075  xpf1o  9071  xpmapenlem  9076  unxpdomlem3  9162  fseqenlem1  9938  fseqenlem2  9939  iundom2g  10454  ordpipq  10857  addpqf  10859  mulpqf  10861  recmulnq  10879  ltexnq  10890  axmulf  11061  cnrecnv  15092  ruclem1  16160  eucalgf  16514  qredeu  16589  crth  16709  phimullem  16710  prmreclem3  16850  setsstruct2  17105  imasaddflem  17455  xpsaddlem  17498  xpsvsca  17502  xpsle  17504  comffval  17626  oppccofval  17643  isoval  17693  brcic  17726  funcf2  17796  idfu2nd  17805  resf2nd  17823  wunfunc  17829  homaval  17959  setcco  18011  catcco  18033  estrcco  18057  xpcco  18110  xpchom2  18113  xpcco2  18114  xpccatid  18115  prfcl  18130  prf1st  18131  prf2nd  18132  evlf2  18145  curf1cl  18155  curf2cl  18158  curfcl  18159  uncf1  18163  uncf2  18164  uncfcurf  18166  diag11  18170  diag12  18171  diag2  18172  curf2ndf  18174  hof2fval  18182  yonedalem21  18200  yonedalem22  18205  yonedalem3b  18206  yonffthlem  18209  latcl2  18363  xpsmnd0  18707  xpsinv  18994  xpsgrpsub  18995  lsmhash  19638  frgpuplem  19705  xpsring1d  20273  rngqiprngimf  21256  pzriprnglem4  21443  pzriprnglem5  21444  pzriprnglem8  21447  pzriprnglem12  21451  mdetrlin  22550  mdetrsca  22551  txcls  23552  txcnp  23568  txcnmpt  23572  txdis1cn  23583  txlly  23584  txnlly  23585  txlm  23596  lmcn2  23597  txkgen  23600  xkococnlem  23607  txhmeo  23751  ptuncnv  23755  txflf  23954  flfcnp2  23955  tmdcn2  24037  qustgplem  24069  tsmsadd  24095  imasdsf1olem  24321  xpsdsval  24329  comet  24461  metustid  24502  metustexhalf  24504  metuel2  24513  tngnm  24599  cnheiborlem  24913  bcthlem5  25288  ovollb2lem  25449  ovolctb  25451  ovoliunlem2  25464  ovolshftlem1  25470  ovolscalem1  25474  ovolicc1  25477  ioombl1lem1  25519  dyadf  25552  itg1addlem4  25660  limccnp2  25853  dvaddbr  25900  dvmulbr  25901  dvmulbrOLD  25902  dvcobr  25909  dvcobrOLD  25910  lhop1lem  25978  cxpcn3  26718  mpodvdsmulf1o  27164  dvdsmulf1o  27166  addsqnreup  27414  addsval  27962  mulsval  28109  tgjustc1  28551  tgjustc2  28552  tgelrnln  28706  numclwwlk1lem2f  30434  ofresid  32723  fsuppcurry1  32805  fsuppcurry2  32806  gsumpart  33148  gsumwrd2dccatlem  33161  gsumwrd2dccat  33162  elrgspnsubrunlem2  33332  erlbrd  33347  rlocaddval  33352  rlocmulval  33353  rloccring  33354  rloc0g  33355  rloc1r  33356  rlocf1  33357  fracerl  33390  fracfld  33392  zringfrac  33637  prsdm  34073  prsrn  34074  esum2dlem  34251  hgt750lemb  34815  cvmlift2lem10  35508  goelel3xp  35544  sat1el2xp  35575  fmla0xp  35579  prv1n  35627  pprodss4v  36078  poimirlem3  37826  poimirlem4  37827  poimirlem17  37840  poimirlem20  37843  mblfinlem2  37861  aks6d1c3  42445  aks6d1c7lem1  42502  f1o2d2  42557  projf1o  45508  ovolval4lem1  46960  ovolval5lem2  46964  gpgiedgdmellem  48359  gpgvtx0  48366  gpgvtx1  48367  gpg3kgrtriex  48402  gpgprismgr4cycllem3  48410  gpgprismgr4cycllem9  48416  tposidres  49198  oppf1st2nd  49443  imaid  49466  xpcfuccocl  49569  swapf1  49584  swapf2val  49585  swapf2  49586  cofuswapf1  49606  cofuswapf2  49607  lanfval  49925  ranfval  49926