Theorem ss2rabi 4100

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

Syntax hints:   → wi 4   ∈ wcel 2108  {crab 3443   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rab 3444  df-ss 3993

This theorem is referenced by:  f1ossf1o  7162  mptexgf  7259  supub  9528  suplub  9529  card2on  9623  rankval4  9936  fin1a2lem12  10480  catlid  17741  catrid  17742  gsumval2  18724  lbsextlem3  21185  psrbagsn  22110  psdmul  22193  musum  27252  ppiub  27266  umgrupgr  29138  umgrislfupgr  29158  usgruspgr  29215  usgrislfuspgr  29222  disjxwwlksn  29937  wwlksnfi  29939  disjxwwlkn  29946  clwwlknclwwlkdifnum  30012  konigsbergssiedgw  30282  omssubadd  34265  bj-unrab  36892  poimirlem26  37606  poimirlem27  37607  ssrabi  38206  lclkrs2  41497  ovolval5lem3  46575