Theorem ss2abi 4045

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

Syntax hints:   → wi 4  {cab 2801   ⊆ wss 3938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-in 3945  df-ss 3954

This theorem is referenced by:  abssi  4048  rabssab  4062  pwpwssunieq  5028  intabs  5247  abssexg  5285  imassrn  5942  fvclss  7003  fabexg  7641  f1oabexg  7644  mapex  8414  tc2  9186  hta  9328  infmap2  9642  cflm  9674  cflim2  9687  hsmex3  9858  domtriomlem  9866  axdc3lem2  9875  brdom7disj  9955  brdom6disj  9956  npex  10410  hashf1lem2  13817  issubc  17107  isghm  18360  permsetex  18500  symgbas  18501  symgbasfi  18509  tgval  21565  ustfn  22812  ustval  22813  ustn0  22831  birthdaylem1  25531  rgrprc  27375  wksfval  27393  mptctf  30455  measbase  31458  measval  31459  ismeas  31460  isrnmeas  31461  ballotlem2  31748  subfaclefac  32425  satfvsuclem1  32608  dfon2lem2  33031  nosupno  33205  poimirlem4  34898  poimirlem9  34903  poimirlem26  34920  poimirlem27  34921  poimirlem28  34922  poimirlem32  34926  sdclem2  35019  lineset  36876  lautset  37220  pautsetN  37236  tendoset  37897  eldiophb  39361  hbtlem1  39730  hbtlem7  39732  relopabVD  41242  rabexgf  41288  prprval  43683  upwlksfval  44017