Theorem ss2rabi 4052

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

Syntax hints:   → wi 4   ∈ wcel 2108  {crab 3415   ⊆ wss 3926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rab 3416  df-ss 3943

This theorem is referenced by:  f1ossf1o  7118  mptexgf  7214  supub  9471  suplub  9472  card2on  9568  rankval4  9881  fin1a2lem12  10425  catlid  17695  catrid  17696  gsumval2  18664  lbsextlem3  21121  psrbagsn  22021  psdmul  22104  musum  27153  ppiub  27167  umgrupgr  29082  umgrislfupgr  29102  usgruspgr  29159  usgrislfuspgr  29166  disjxwwlksn  29886  wwlksnfi  29888  disjxwwlkn  29895  clwwlknclwwlkdifnum  29961  konigsbergssiedgw  30231  omssubadd  34332  bj-unrab  36944  poimirlem26  37670  poimirlem27  37671  ssrabi  38268  lclkrs2  41559  ovolval5lem3  46683