Theorem ss2rabi 4036

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

Syntax hints:   → wi 4   ∈ wcel 2109  {crab 3402   ⊆ wss 3911

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rab 3403  df-ss 3928

This theorem is referenced by:  f1ossf1o  7082  mptexgf  7178  supub  9386  suplub  9387  card2on  9483  rankval4  9796  fin1a2lem12  10340  catlid  17620  catrid  17621  gsumval2  18589  lbsextlem3  21046  psrbagsn  21946  psdmul  22029  musum  27077  ppiub  27091  umgrupgr  29006  umgrislfupgr  29026  usgruspgr  29083  usgrislfuspgr  29090  disjxwwlksn  29807  wwlksnfi  29809  disjxwwlkn  29816  clwwlknclwwlkdifnum  29882  konigsbergssiedgw  30152  omssubadd  34264  bj-unrab  36887  poimirlem26  37613  poimirlem27  37614  ssrabi  38212  lclkrs2  41507  ovolval5lem3  46625