Theorem ss2rabi 4040

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

Syntax hints:   → wi 4   ∈ wcel 2109  {crab 3405   ⊆ wss 3914

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 3406  df-ss 3931

This theorem is referenced by:  f1ossf1o  7100  mptexgf  7196  supub  9410  suplub  9411  card2on  9507  rankval4  9820  fin1a2lem12  10364  catlid  17644  catrid  17645  gsumval2  18613  lbsextlem3  21070  psrbagsn  21970  psdmul  22053  musum  27101  ppiub  27115  umgrupgr  29030  umgrislfupgr  29050  usgruspgr  29107  usgrislfuspgr  29114  disjxwwlksn  29834  wwlksnfi  29836  disjxwwlkn  29843  clwwlknclwwlkdifnum  29909  konigsbergssiedgw  30179  omssubadd  34291  bj-unrab  36914  poimirlem26  37640  poimirlem27  37641  ssrabi  38239  lclkrs2  41534  ovolval5lem3  46652