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

Theorem prssd 4739
Description: Deduction version of prssi 4738: A pair of elements of a class is a subset of the class. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
prssd.1 (𝜑𝐴𝐶)
prssd.2 (𝜑𝐵𝐶)
Assertion
Ref Expression
prssd (𝜑 → {𝐴, 𝐵} ⊆ 𝐶)

Proof of Theorem prssd
StepHypRef Expression
1 prssd.1 . 2 (𝜑𝐴𝐶)
2 prssd.2 . 2 (𝜑𝐵𝐶)
3 prssi 4738 . 2 ((𝐴𝐶𝐵𝐶) → {𝐴, 𝐵} ⊆ 𝐶)
41, 2, 3syl2anc 587 1 (𝜑 → {𝐴, 𝐵} ⊆ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2115  wss 3919  {cpr 4552
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 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-un 3924  df-in 3926  df-ss 3936  df-sn 4551  df-pr 4553
This theorem is referenced by:  fpr2g  6967  f1prex  7034  fveqf1o  7053  fr3nr  7490  en2eqpr  9433  en2eleq  9434  r0weon  9438  wuncval2  10169  nehash2  13839  1idssfct  16024  basprssdmsets  16551  mrcun  16895  joinval2  17621  meetval2  17635  0idnsgd  18325  pmtrprfv  18583  pmtrprfv3  18584  symggen  18600  pmtr3ncomlem1  18603  psgnunilem1  18623  lspprcl  19752  lsptpcl  19753  lspprss  19766  lspprid1  19771  lsppratlem2  19922  lsppratlem3  19923  lsppratlem4  19924  drngnidl  20004  drnglpir  20028  mdetralt  21222  topgele  21544  pptbas  21622  isconn2  22028  xpsdsval  22997  itgioo  24428  wilthlem2  25663  perfectlem2  25823  upgrex  26894  upgr1e  26915  uspgr1e  27043  eupth2lems  28032  s2f1  30642  pmtrcnel  30775  pmtrcnel2  30776  pmtridf1o  30778  cycpm2tr  30803  cyc3co2  30824  cyc3evpm  30834  cyc3genpmlem  30835  cyc3conja  30841  linds2eq  30987  poimirlem9  35038  clsk1indlem4  40694  clsk1indlem1  40695  mnuprssd  40925  mnuprdlem4  40931  limsup10exlem  42367  meadjun  43054  line2  45119  line2y  45122
  Copyright terms: Public domain W3C validator