Theorem opelxpd 5673

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

Syntax hints:   → wi 4   ∈ wcel 2114  ⟨cop 4588   × cxp 5632

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 5245  ax-pr 5381

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 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-opab 5163  df-xp 5640

This theorem is referenced by:  otel3xp  5680  opabssxpd  5681  relssdmrn  6237  fpr2g  7169  fliftrel  7266  elovimad  7420  el2xptp0  7992  oprab2co  8051  1stconst  8054  2ndconst  8055  curry2  8061  fsplitfpar  8072  offsplitfpar  8073  fnwelem  8085  xpf1o  9081  xpmapenlem  9086  unxpdomlem3  9172  fseqenlem1  9948  fseqenlem2  9949  iundom2g  10464  ordpipq  10867  addpqf  10869  mulpqf  10871  recmulnq  10889  ltexnq  10900  axmulf  11071  cnrecnv  15102  ruclem1  16170  eucalgf  16524  qredeu  16599  crth  16719  phimullem  16720  prmreclem3  16860  setsstruct2  17115  imasaddflem  17465  xpsaddlem  17508  xpsvsca  17512  xpsle  17514  comffval  17636  oppccofval  17653  isoval  17703  brcic  17736  funcf2  17806  idfu2nd  17815  resf2nd  17833  wunfunc  17839  homaval  17969  setcco  18021  catcco  18043  estrcco  18067  xpcco  18120  xpchom2  18123  xpcco2  18124  xpccatid  18125  prfcl  18140  prf1st  18141  prf2nd  18142  evlf2  18155  curf1cl  18165  curf2cl  18168  curfcl  18169  uncf1  18173  uncf2  18174  uncfcurf  18176  diag11  18180  diag12  18181  diag2  18182  curf2ndf  18184  hof2fval  18192  yonedalem21  18210  yonedalem22  18215  yonedalem3b  18216  yonffthlem  18219  latcl2  18373  xpsmnd0  18717  xpsinv  19007  xpsgrpsub  19008  lsmhash  19651  frgpuplem  19718  xpsring1d  20286  rngqiprngimf  21269  pzriprnglem4  21456  pzriprnglem5  21457  pzriprnglem8  21460  pzriprnglem12  21464  mdetrlin  22563  mdetrsca  22564  txcls  23565  txcnp  23581  txcnmpt  23585  txdis1cn  23596  txlly  23597  txnlly  23598  txlm  23609  lmcn2  23610  txkgen  23613  xkococnlem  23620  txhmeo  23764  ptuncnv  23768  txflf  23967  flfcnp2  23968  tmdcn2  24050  qustgplem  24082  tsmsadd  24108  imasdsf1olem  24334  xpsdsval  24342  comet  24474  metustid  24515  metustexhalf  24517  metuel2  24526  tngnm  24612  cnheiborlem  24926  bcthlem5  25301  ovollb2lem  25462  ovolctb  25464  ovoliunlem2  25477  ovolshftlem1  25483  ovolscalem1  25487  ovolicc1  25490  ioombl1lem1  25532  dyadf  25565  itg1addlem4  25673  limccnp2  25866  dvaddbr  25913  dvmulbr  25914  dvmulbrOLD  25915  dvcobr  25922  dvcobrOLD  25923  lhop1lem  25991  cxpcn3  26731  mpodvdsmulf1o  27177  dvdsmulf1o  27179  addsqnreup  27427  addsval  27975  mulsval  28122  tgjustc1  28565  tgjustc2  28566  tgelrnln  28720  numclwwlk1lem2f  30448  ofresid  32738  fsuppcurry1  32820  fsuppcurry2  32821  gsumpart  33163  gsumwrd2dccatlem  33177  gsumwrd2dccat  33178  elrgspnsubrunlem2  33348  erlbrd  33363  rlocaddval  33368  rlocmulval  33369  rloccring  33370  rloc0g  33371  rloc1r  33372  rlocf1  33373  fracerl  33406  fracfld  33408  zringfrac  33653  prsdm  34098  prsrn  34099  esum2dlem  34276  hgt750lemb  34840  cvmlift2lem10  35534  goelel3xp  35570  sat1el2xp  35601  fmla0xp  35605  prv1n  35653  pprodss4v  36104  poimirlem3  37903  poimirlem4  37904  poimirlem17  37917  poimirlem20  37920  mblfinlem2  37938  aks6d1c3  42522  aks6d1c7lem1  42579  f1o2d2  42634  projf1o  45584  hoicvr  46935  ovolval4lem1  47036  ovolval5lem2  47040  gpgiedgdmellem  48435  gpgvtx0  48442  gpgvtx1  48443  gpg3kgrtriex  48478  gpgprismgr4cycllem3  48486  gpgprismgr4cycllem9  48492  tposidres  49274  oppf1st2nd  49519  imaid  49542  xpcfuccocl  49645  swapf1  49660  swapf2val  49661  swapf2  49662  cofuswapf1  49682  cofuswapf2  49683  lanfval  50001  ranfval  50002