Theorem ss2abi 3834

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

Syntax hints:   → wi 4  {cab 2751   ⊆ wss 3732

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-in 3739  df-ss 3746

This theorem is referenced by:  abssi  3837  rabssab  3851  pwpwssunieq  4772  intabs  4983  abssexg  5017  imassrn  5659  fvclss  6692  fabexg  7320  f1oabexg  7323  mapex  8066  tc2  8833  hta  8975  infmap2  9293  cflm  9325  cflim2  9338  hsmex3  9509  domtriomlem  9517  axdc3lem2  9526  brdom7disj  9606  brdom6disj  9607  npex  10061  hashf1lem2  13441  issubc  16760  isghm  17924  symgbasfi  18069  tgval  21039  ustfn  22284  ustval  22285  ustn0  22303  birthdaylem1  24969  rgrprc  26778  wksfval  26796  mptctf  29944  measbase  30707  measval  30708  ismeas  30709  isrnmeas  30710  ballotlem2  30998  subfaclefac  31606  dfon2lem2  32132  nosupno  32293  cnfinltrel  33674  poimirlem4  33837  poimirlem9  33842  poimirlem26  33859  poimirlem27  33860  poimirlem28  33861  poimirlem32  33865  sdclem2  33960  lineset  35694  lautset  36038  pautsetN  36054  tendoset  36715  eldiophb  37998  hbtlem1  38370  hbtlem7  38372  relopabVD  39789  rabexgf  39835  upwlksfval  42385