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

Theorem ss2abi 3707
 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 3703 . 2 ({𝑥𝜑} ⊆ {𝑥𝜓} ↔ ∀𝑥(𝜑𝜓))
2 ss2abi.1 . 2 (𝜑𝜓)
31, 2mpgbir 1766 1 {𝑥𝜑} ⊆ {𝑥𝜓}
 Colors of variables: wff setvar class Syntax hints:   → wi 4  {cab 2637   ⊆ wss 3607 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-in 3614  df-ss 3621 This theorem is referenced by:  abssi  3710  rabssab  3723  pwpwssunieq  4647  intabs  4855  abssexg  4881  imassrn  5512  fvclss  6540  fabexg  7164  f1oabexg  7167  mapex  7905  tc2  8656  hta  8798  infmap2  9078  cflm  9110  cflim2  9123  hsmex3  9294  domtriomlem  9302  axdc3lem2  9311  brdom7disj  9391  brdom6disj  9392  npex  9846  hashf1lem2  13278  issubc  16542  isghm  17707  symgbasfi  17852  tgval  20807  ustfn  22052  ustval  22053  ustn0  22071  birthdaylem1  24723  rgrprc  26543  wksfval  26561  mptctf  29623  measbase  30388  measval  30389  ismeas  30390  isrnmeas  30391  ballotlem2  30678  subfaclefac  31284  dfon2lem2  31813  nosupno  31974  poimirlem4  33543  poimirlem9  33548  poimirlem26  33565  poimirlem27  33566  poimirlem28  33567  poimirlem32  33571  sdclem2  33668  lineset  35342  lautset  35686  pautsetN  35702  tendoset  36364  eldiophb  37637  hbtlem1  38010  hbtlem7  38012  relopabVD  39451  rabexgf  39497  upwlksfval  42041
 Copyright terms: Public domain W3C validator