Theorem ss2rabi 3905

Description: Inference of restricted abstraction subclass from implication. (Contributed by NM, 14-Oct-1999.)

Hypothesis

Ref	Expression
ss2rabi.1	⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))

Assertion

Ref	Expression
ss2rabi	⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓}

Proof of Theorem ss2rabi

Step	Hyp	Ref	Expression
1		ss2rab 3899	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
2		ss2rabi.1	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	1, 2	mprgbir 3109	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ∈ wcel 2107  {crab 3094   ⊆ 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-ral 3095  df-rab 3099  df-in 3799  df-ss 3806

This theorem is referenced by:  f1ossf1o  6660  supub  8653  suplub  8654  card2on  8748  rankval4  9027  fin1a2lem12  9568  catlid  16729  catrid  16730  gsumval2  17666  lbsextlem3  19557  psrbagsn  19891  musum  25369  ppiub  25381  umgrupgr  26451  umgrislfupgr  26471  usgruspgr  26527  usgrislfuspgr  26533  disjxwwlksn  27275  disjxwwlksnOLD  27276  clwwlknclwwlkdifnum  27360  konigsbergssiedgw  27656  omssubadd  30960  bj-unrab  33496  poimirlem26  34061  poimirlem27  34062  ssrabi  34649  lclkrs2  37694