Theorem ss2abi 4042

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

Syntax hints:   → wi 4  {cab 2799   ⊆ wss 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-in 3942  df-ss 3951

This theorem is referenced by:  abssi  4045  rabssab  4059  pwpwssunieq  5025  intabs  5244  abssexg  5282  imassrn  5939  fvclss  7000  fabexg  7638  f1oabexg  7641  mapex  8411  tc2  9183  hta  9325  infmap2  9639  cflm  9671  cflim2  9684  hsmex3  9855  domtriomlem  9863  axdc3lem2  9872  brdom7disj  9952  brdom6disj  9953  npex  10407  hashf1lem2  13813  issubc  17104  isghm  18357  permsetex  18497  symgbas  18498  symgbasfi  18506  tgval  21562  ustfn  22809  ustval  22810  ustn0  22828  birthdaylem1  25528  rgrprc  27372  wksfval  27390  mptctf  30452  measbase  31456  measval  31457  ismeas  31458  isrnmeas  31459  ballotlem2  31746  subfaclefac  32423  satfvsuclem1  32606  dfon2lem2  33029  nosupno  33203  poimirlem4  34895  poimirlem9  34900  poimirlem26  34917  poimirlem27  34918  poimirlem28  34919  poimirlem32  34923  sdclem2  35016  lineset  36873  lautset  37217  pautsetN  37233  tendoset  37894  eldiophb  39352  hbtlem1  39721  hbtlem7  39723  relopabVD  41233  rabexgf  41279  prprval  43675  upwlksfval  44009