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

Theorem opelxpd 5561
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 5560 . 2 ((𝐴𝐶𝐵𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
41, 2, 3syl2anc 587 1 (𝜑 → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  cop 4534   × cxp 5521
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-opab 5096  df-xp 5529
This theorem is referenced by:  otel3xp  5567  opabssxpd  5757  fpr2g  6955  fliftrel  7044  elovimad  7187  el2xptp0  7722  oprab2co  7779  1stconst  7782  2ndconst  7783  curry2  7789  fsplitfpar  7801  offsplitfpar  7802  fnwelem  7812  xpf1o  8667  xpmapenlem  8672  unxpdomlem3  8712  fseqenlem1  9439  fseqenlem2  9440  iundom2g  9955  ordpipq  10357  addpqf  10359  mulpqf  10361  recmulnq  10379  ltexnq  10390  axmulf  10561  cnrecnv  14519  ruclem1  15579  eucalgf  15920  qredeu  15995  crth  16108  phimullem  16109  prmreclem3  16247  setsstruct2  16516  imasaddflem  16798  xpsaddlem  16841  xpsvsca  16845  xpsle  16847  comffval  16964  oppccofval  16981  isoval  17030  brcic  17063  funcf2  17133  idfu2nd  17142  resf2nd  17160  wunfunc  17164  homaval  17286  setcco  17338  catcco  17356  estrcco  17375  xpcco  17428  xpchom2  17431  xpcco2  17432  xpccatid  17433  prfcl  17448  prf1st  17449  prf2nd  17450  evlf2  17463  curf1cl  17473  curf2cl  17476  curfcl  17477  uncf1  17481  uncf2  17482  uncfcurf  17484  diag11  17488  diag12  17489  diag2  17490  curf2ndf  17492  hof2fval  17500  yonedalem21  17518  yonedalem22  17523  yonedalem3b  17524  yonffthlem  17527  latcl2  17653  lsmhash  18826  frgpuplem  18893  mdetrlin  21210  mdetrsca  21211  txcls  22212  txcnp  22228  txcnmpt  22232  txdis1cn  22243  txlly  22244  txnlly  22245  txlm  22256  lmcn2  22257  txkgen  22260  xkococnlem  22267  txhmeo  22411  ptuncnv  22415  txflf  22614  flfcnp2  22615  tmdcn2  22697  qustgplem  22729  tsmsadd  22755  imasdsf1olem  22983  xpsdsval  22991  comet  23123  metustid  23164  metustexhalf  23166  metuel2  23175  tngnm  23260  cnheiborlem  23562  bcthlem5  23935  ovollb2lem  24095  ovolctb  24097  ovoliunlem2  24110  ovolshftlem1  24116  ovolscalem1  24120  ovolicc1  24123  ioombl1lem1  24165  dyadf  24198  itg1addlem4  24306  limccnp2  24498  dvaddbr  24544  dvmulbr  24545  dvcobr  24552  lhop1lem  24619  cxpcn3  25340  dvdsmulf1o  25782  addsqnreup  26030  tgjustc1  26272  tgjustc2  26273  tgelrnln  26427  numclwwlk1lem2f  28143  ofresid  30406  fsuppcurry1  30490  fsuppcurry2  30491  gsumpart  30743  prsdm  31265  prsrn  31266  esum2dlem  31459  hgt750lemb  32035  cvmlift2lem10  32667  goelel3xp  32703  sat1el2xp  32734  fmla0xp  32738  prv1n  32786  pprodss4v  33453  mblfinlem2  35088  projf1o  41812  ovolval4lem1  43275  ovolval5lem2  43279
  Copyright terms: Public domain W3C validator