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

Theorem opelxpd 5586
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 5585 . 2 ((𝐴𝐶𝐵𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
41, 2, 3syl2anc 584 1 (𝜑 → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  cop 4563   × cxp 5546
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-opab 5120  df-xp 5554
This theorem is referenced by:  otel3xp  5592  opabssxpd  5782  fpr2g  6965  fliftrel  7050  elovimad  7193  el2xptp0  7725  oprab2co  7781  1stconst  7784  2ndconst  7785  curry2  7791  fsplitfpar  7803  offsplitfpar  7804  fnwelem  7814  xpf1o  8667  xpmapenlem  8672  unxpdomlem3  8712  fseqenlem1  9438  fseqenlem2  9439  iundom2g  9950  ordpipq  10352  addpqf  10354  mulpqf  10356  recmulnq  10374  ltexnq  10385  axmulf  10556  cnrecnv  14512  ruclem1  15572  eucalgf  15915  qredeu  15990  crth  16103  phimullem  16104  prmreclem3  16242  setsstruct2  16509  imasaddflem  16791  xpsaddlem  16834  xpsvsca  16838  xpsle  16840  comffval  16957  oppccofval  16974  isoval  17023  brcic  17056  funcf2  17126  idfu2nd  17135  resf2nd  17153  wunfunc  17157  homaval  17279  setcco  17331  catcco  17349  estrcco  17368  xpcco  17421  xpchom2  17424  xpcco2  17425  xpccatid  17426  prfcl  17441  prf1st  17442  prf2nd  17443  evlf2  17456  curf1cl  17466  curf2cl  17469  curfcl  17470  uncf1  17474  uncf2  17475  uncfcurf  17477  diag11  17481  diag12  17482  diag2  17483  curf2ndf  17485  hof2fval  17493  yonedalem21  17511  yonedalem22  17516  yonedalem3b  17517  yonffthlem  17520  latcl2  17646  lsmhash  18760  frgpuplem  18827  mdetrlin  21139  mdetrsca  21140  txcls  22140  txcnp  22156  txcnmpt  22160  txdis1cn  22171  txlly  22172  txnlly  22173  txlm  22184  lmcn2  22185  txkgen  22188  xkococnlem  22195  txhmeo  22339  ptuncnv  22343  txflf  22542  flfcnp2  22543  tmdcn2  22625  qustgplem  22656  tsmsadd  22682  imasdsf1olem  22910  xpsdsval  22918  comet  23050  metustid  23091  metustexhalf  23093  metuel2  23102  tngnm  23187  cnheiborlem  23485  bcthlem5  23858  ovollb2lem  24016  ovolctb  24018  ovoliunlem2  24031  ovolshftlem1  24037  ovolscalem1  24041  ovolicc1  24044  ioombl1lem1  24086  dyadf  24119  itg1addlem4  24227  limccnp2  24417  dvaddbr  24462  dvmulbr  24463  dvcobr  24470  lhop1lem  24537  cxpcn3  25256  dvdsmulf1o  25698  addsqnreup  25946  tgjustc1  26188  tgjustc2  26189  tgelrnln  26343  numclwwlk1lem2f  28061  ofresid  30317  fsuppcurry1  30387  fsuppcurry2  30388  prsdm  31056  prsrn  31057  esum2dlem  31250  hgt750lemb  31826  cvmlift2lem10  32456  goelel3xp  32492  sat1el2xp  32523  fmla0xp  32527  prv1n  32575  pprodss4v  33242  mblfinlem2  34811  projf1o  41335  ovolval4lem1  42808  ovolval5lem2  42812
  Copyright terms: Public domain W3C validator