Theorem ss2rabi 4028

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

Syntax hints:   → wi 4   ∈ wcel 2109  {crab 3394   ⊆ wss 3903

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 3395  df-ss 3920

This theorem is referenced by:  f1ossf1o  7062  mptexgf  7158  supub  9349  suplub  9350  card2on  9446  rankval4  9763  fin1a2lem12  10305  catlid  17589  catrid  17590  gsumval2  18560  lbsextlem3  21067  psrbagsn  21968  psdmul  22051  musum  27099  ppiub  27113  umgrupgr  29048  umgrislfupgr  29068  usgruspgr  29125  usgrislfuspgr  29132  disjxwwlksn  29849  wwlksnfi  29851  disjxwwlkn  29858  clwwlknclwwlkdifnum  29924  konigsbergssiedgw  30194  omssubadd  34268  bj-unrab  36900  poimirlem26  37626  poimirlem27  37627  ssrabi  38225  lclkrs2  41519  ovolval5lem3  46635