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  17624  catrid  17625  gsumval2  18595  lbsextlem3  21102  psrbagsn  22003  psdmul  22086  musum  27134  ppiub  27148  umgrupgr  29083  umgrislfupgr  29103  usgruspgr  29160  usgrislfuspgr  29167  disjxwwlksn  29884  wwlksnfi  29886  disjxwwlkn  29893  clwwlknclwwlkdifnum  29959  konigsbergssiedgw  30229  omssubadd  34284  bj-unrab  36907  poimirlem26  37633  poimirlem27  37634  ssrabi  38232  lclkrs2  41527  ovolval5lem3  46645