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

Theorem ss2abi 4029
Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.)
Hypothesis
Ref Expression
ss2abi.1 (𝜑𝜓)
Assertion
Ref Expression
ss2abi {𝑥𝜑} ⊆ {𝑥𝜓}

Proof of Theorem ss2abi
StepHypRef Expression
1 ss2ab 4025 . 2 ({𝑥𝜑} ⊆ {𝑥𝜓} ↔ ∀𝑥(𝜑𝜓))
2 ss2abi.1 . 2 (𝜑𝜓)
31, 2mpgbir 1801 1 {𝑥𝜑} ⊆ {𝑥𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  {cab 2802  wss 3919
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-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-v 3482  df-in 3926  df-ss 3936
This theorem is referenced by:  abssi  4032  rabssab  4046  pwpwssunieq  5012  intabs  5232  abssexg  5271  imassrn  5929  fvclss  6995  fabexg  7636  f1oabexg  7639  mapex  8410  tc2  9183  hta  9325  infmap2  9640  cflm  9672  cflim2  9685  hsmex3  9856  domtriomlem  9864  axdc3lem2  9873  brdom7disj  9953  brdom6disj  9954  npex  10408  hashf1lem2  13821  issubc  17107  isghm  18360  permsetex  18500  symgbas  18501  symgbasfi  18509  tgval  21569  ustfn  22816  ustval  22817  ustn0  22835  birthdaylem1  25546  rgrprc  27390  wksfval  27408  mptctf  30474  measbase  31541  measval  31542  ismeas  31543  isrnmeas  31544  ballotlem2  31831  subfaclefac  32508  satfvsuclem1  32691  dfon2lem2  33114  nosupno  33288  poimirlem4  35033  poimirlem9  35038  poimirlem26  35055  poimirlem27  35056  poimirlem28  35057  poimirlem32  35061  sdclem2  35152  lineset  37006  lautset  37350  pautsetN  37366  tendoset  38027  eldiophb  39642  hbtlem1  40011  hbtlem7  40013  relopabVD  41555  rabexgf  41601  prprval  43984  upwlksfval  44316
  Copyright terms: Public domain W3C validator