Theorem ss2rabi 4023

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

Syntax hints:   → wi 4   ∈ wcel 2111  {crab 3395   ⊆ wss 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rab 3396  df-ss 3914

This theorem is referenced by:  f1ossf1o  7061  mptexgf  7156  supub  9343  suplub  9344  card2on  9440  rankval4  9760  fin1a2lem12  10302  catlid  17589  catrid  17590  gsumval2  18594  lbsextlem3  21097  psrbagsn  21998  psdmul  22081  musum  27128  ppiub  27142  umgrupgr  29081  umgrislfupgr  29101  usgruspgr  29158  usgrislfuspgr  29165  disjxwwlksn  29882  wwlksnfi  29884  disjxwwlkn  29891  clwwlknclwwlkdifnum  29960  konigsbergssiedgw  30230  omssubadd  34313  bj-unrab  36968  poimirlem26  37694  poimirlem27  37695  ssrabi  38293  lclkrs2  41587  ovolval5lem3  46700