Theorem ss2abi 3895

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

Step	Hyp	Ref	Expression
1		ss2ab 3891	. 2 ⊢ ({𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓} ↔ ∀𝑥(𝜑 → 𝜓))
2		ss2abi.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	mpgbir 1843	1 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}

Syntax hints:   → wi 4  {cab 2763   ⊆ wss 3792

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-in 3799  df-ss 3806

This theorem is referenced by:  abssi  3898  rabssab  3912  pwpwssunieq  4849  intabs  5059  abssexg  5093  imassrn  5731  fvclss  6772  fabexg  7401  f1oabexg  7404  mapex  8146  tc2  8915  hta  9057  infmap2  9375  cflm  9407  cflim2  9420  hsmex3  9591  domtriomlem  9599  axdc3lem2  9608  brdom7disj  9688  brdom6disj  9689  npex  10143  hashf1lem2  13554  issubc  16880  isghm  18044  symgbasfi  18189  tgval  21167  ustfn  22413  ustval  22414  ustn0  22432  birthdaylem1  25130  rgrprc  26939  wksfval  26957  mptctf  30061  measbase  30858  measval  30859  ismeas  30860  isrnmeas  30861  ballotlem2  31149  subfaclefac  31757  dfon2lem2  32277  nosupno  32438  cnfinltrel  33836  poimirlem4  34041  poimirlem9  34046  poimirlem26  34063  poimirlem27  34064  poimirlem28  34065  poimirlem32  34069  sdclem2  34164  lineset  35894  lautset  36238  pautsetN  36254  tendoset  36915  eldiophb  38284  hbtlem1  38656  hbtlem7  38658  relopabVD  40074  rabexgf  40120  prprval  42457  upwlksfval  42762