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  6662  supub  8655  suplub  8656  card2on  8750  rankval4  9029  fin1a2lem12  9570  catlid  16733  catrid  16734  gsumval2  17670  lbsextlem3  19561  psrbagsn  19895  musum  25373  ppiub  25385  umgrupgr  26455  umgrislfupgr  26475  usgruspgr  26531  usgrislfuspgr  26537  disjxwwlksn  27279  disjxwwlksnOLD  27280  clwwlknclwwlkdifnum  27364  konigsbergssiedgw  27660  omssubadd  30964  bj-unrab  33500  poimirlem26  34066  poimirlem27  34067  ssrabi  34654  lclkrs2  37699