Theorem ss2rabi 4010

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 4004	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
2		ss2rabi.1	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	1, 2	mprgbir 3079	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ∈ wcel 2106  {crab 3068   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  f1ossf1o  7000  supub  9218  suplub  9219  card2on  9313  rankval4  9625  fin1a2lem12  10167  catlid  17392  catrid  17393  gsumval2  18370  lbsextlem3  20422  psrbagsn  21271  musum  26340  ppiub  26352  umgrupgr  27473  umgrislfupgr  27493  usgruspgr  27548  usgrislfuspgr  27554  disjxwwlksn  28269  clwwlknclwwlkdifnum  28344  konigsbergssiedgw  28614  omssubadd  32267  bj-unrab  35114  poimirlem26  35803  poimirlem27  35804  ssrabi  36389  lclkrs2  39554