MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opelxpd Structured version   Visualization version   GIF version

Theorem opelxpd 5675
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
StepHypRef Expression
1 opelxpd.1 . 2 (𝜑𝐴𝐶)
2 opelxpd.2 . 2 (𝜑𝐵𝐷)
3 opelxpi 5674 . 2 ((𝐴𝐶𝐵𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
41, 2, 3syl2anc 585 1 (𝜑 → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cop 4596   × cxp 5635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5260  ax-nul 5267  ax-pr 5388
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-sn 4591  df-pr 4593  df-op 4597  df-opab 5172  df-xp 5643
This theorem is referenced by:  otel3xp  5682  opabssxpd  5683  relssdmrn  6224  fpr2g  7165  fliftrel  7257  elovimad  7409  el2xptp0  7972  oprab2co  8033  1stconst  8036  2ndconst  8037  curry2  8043  fsplitfpar  8054  offsplitfpar  8055  fnwelem  8067  xpf1o  9089  xpmapenlem  9094  unxpdomlem3  9202  fseqenlem1  9968  fseqenlem2  9969  iundom2g  10484  ordpipq  10886  addpqf  10888  mulpqf  10890  recmulnq  10908  ltexnq  10919  axmulf  11090  cnrecnv  15059  ruclem1  16121  eucalgf  16467  qredeu  16542  crth  16658  phimullem  16659  prmreclem3  16798  setsstruct2  17054  imasaddflem  17420  xpsaddlem  17463  xpsvsca  17467  xpsle  17469  comffval  17587  oppccofval  17605  isoval  17656  brcic  17689  funcf2  17762  idfu2nd  17771  resf2nd  17789  wunfunc  17793  wunfuncOLD  17794  homaval  17925  setcco  17977  catcco  17999  estrcco  18025  xpcco  18079  xpchom2  18082  xpcco2  18083  xpccatid  18084  prfcl  18099  prf1st  18100  prf2nd  18101  evlf2  18115  curf1cl  18125  curf2cl  18128  curfcl  18129  uncf1  18133  uncf2  18134  uncfcurf  18136  diag11  18140  diag12  18141  diag2  18142  curf2ndf  18144  hof2fval  18152  yonedalem21  18170  yonedalem22  18175  yonedalem3b  18176  yonffthlem  18179  latcl2  18333  lsmhash  19495  frgpuplem  19562  mdetrlin  21974  mdetrsca  21975  txcls  22978  txcnp  22994  txcnmpt  22998  txdis1cn  23009  txlly  23010  txnlly  23011  txlm  23022  lmcn2  23023  txkgen  23026  xkococnlem  23033  txhmeo  23177  ptuncnv  23181  txflf  23380  flfcnp2  23381  tmdcn2  23463  qustgplem  23495  tsmsadd  23521  imasdsf1olem  23749  xpsdsval  23757  comet  23892  metustid  23933  metustexhalf  23935  metuel2  23944  tngnm  24038  cnheiborlem  24340  bcthlem5  24715  ovollb2lem  24875  ovolctb  24877  ovoliunlem2  24890  ovolshftlem1  24896  ovolscalem1  24900  ovolicc1  24903  ioombl1lem1  24945  dyadf  24978  itg1addlem4  25086  itg1addlem4OLD  25087  limccnp2  25279  dvaddbr  25325  dvmulbr  25326  dvcobr  25333  lhop1lem  25400  cxpcn3  26124  dvdsmulf1o  26566  addsqnreup  26814  addsval  27303  mulsval  27403  tgjustc1  27466  tgjustc2  27467  tgelrnln  27621  numclwwlk1lem2f  29348  ofresid  31611  fsuppcurry1  31696  fsuppcurry2  31697  gsumpart  31953  prsdm  32559  prsrn  32560  esum2dlem  32755  hgt750lemb  33333  cvmlift2lem10  33970  goelel3xp  34006  sat1el2xp  34037  fmla0xp  34041  prv1n  34089  pprodss4v  34522  poimirlem3  36131  poimirlem4  36132  poimirlem17  36145  poimirlem20  36148  mblfinlem2  36166  projf1o  43509  ovolval4lem1  44980  ovolval5lem2  44984
  Copyright terms: Public domain W3C validator