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

Theorem prssd 4747
Description: Deduction version of prssi 4746: 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 4746 . 2 ((𝐴𝐶𝐵𝐶) → {𝐴, 𝐵} ⊆ 𝐶)
41, 2, 3syl2anc 584 1 (𝜑 → {𝐴, 𝐵} ⊆ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  wss 3933  {cpr 4559
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
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-v 3494  df-un 3938  df-in 3940  df-ss 3949  df-sn 4558  df-pr 4560
This theorem is referenced by:  fpr2g  6965  f1prex  7031  fveqf1o  7049  fr3nr  7483  en2eqpr  9421  en2eleq  9422  r0weon  9426  wuncval2  10157  nehash2  13820  1idssfct  16012  basprssdmsets  16537  mrcun  16881  joinval2  17607  meetval2  17621  0idnsgd  18261  pmtrprfv  18510  pmtrprfv3  18511  symggen  18527  pmtr3ncomlem1  18530  psgnunilem1  18550  lspprcl  19679  lsptpcl  19680  lspprss  19693  lspprid1  19698  lsppratlem2  19849  lsppratlem3  19850  lsppratlem4  19851  drngnidl  19930  drnglpir  19954  mdetralt  21145  topgele  21466  pptbas  21544  isconn2  21950  xpsdsval  22918  itgioo  24343  wilthlem2  25573  perfectlem2  25733  upgrex  26804  upgr1e  26825  uspgr1e  26953  eupth2lems  27944  s2f1  30548  pmtrcnel  30660  pmtrcnel2  30661  pmtridf1o  30663  cycpm2tr  30688  cyc3co2  30709  cyc3evpm  30719  cyc3genpmlem  30720  cyc3conja  30726  linds2eq  30868  poimirlem9  34782  clsk1indlem4  40272  clsk1indlem1  40273  mnuprssd  40482  mnuprdlem4  40488  limsup10exlem  41929  meadjun  42621  line2  44667  line2y  44670
  Copyright terms: Public domain W3C validator