Theorem ss2abi 3637

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 3633	. 2 ⊢ ({𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓} ↔ ∀𝑥(𝜑 → 𝜓))
2		ss2abi.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	mpgbir 1717	1 ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}

Syntax hints:   → wi 4  {cab 2596   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-in 3547  df-ss 3554

This theorem is referenced by:  abssi  3640  rabssab  3652  intabs  4752  abssexg  4777  imassrn  5396  fvclss  6404  fabexg  7015  f1oabexg  7018  mapex  7750  tc2  8501  hta  8643  infmap2  8923  cflm  8955  cflim2  8968  hsmex3  9139  domtriomlem  9147  axdc3lem2  9156  brdom7disj  9234  brdom6disj  9235  npex  9687  hashf1lem2  13097  issubc  16318  isghm  17483  symgbasfi  17629  tgval  20570  ustfn  21815  ustval  21816  ustn0  21834  birthdaylem1  24478  wlks  26047  trls  26066  mptctf  28883  measbase  29587  measval  29588  ismeas  29589  isrnmeas  29590  ballotlem2  29877  subfaclefac  30412  dfon2lem2  30933  bj-sspwpweq  32240  poimirlem4  32583  poimirlem9  32588  poimirlem26  32605  poimirlem27  32606  poimirlem28  32607  poimirlem32  32611  sdclem2  32708  lineset  34042  lautset  34386  pautsetN  34402  tendoset  35065  eldiophb  36338  hbtlem1  36712  hbtlem7  36714  relopabVD  38159  rabexgf  38206  rgrprc  40791  1wlksfval  40811  wlksfval  40812