Theorem ss2rabi 4024

Description: Inference of restricted abstraction subclass from implication. (Contributed by NM, 14-Oct-1999.) Avoid axioms. (Revised by SN, 4-Feb-2025.)

Hypothesis

Ref	Expression
ss2rabi.1	⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))

Assertion

Ref	Expression
ss2rabi	⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓}

Proof of Theorem ss2rabi

Step	Hyp	Ref	Expression
1		ss2rabi.1	. . . 4 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
2	1	adantl 487	. . 3 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐴) → (𝜑 → 𝜓))
3	2	ss2rabdv 4023	. 2 ⊢ (⊤ → {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓})
4	3	mptru 1577	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓}

This proof depends on syntax axioms:   → wi 4  ⊤wtru 1571   ∈ wcel 2145  {crab 3413   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-ral 3078  df-rab 3414  df-ss 3916

This theorem is used by:  f1ossf1o  7127  mptexgf  7226  supub  9444  suplub  9445  card2on  9541  rankval4  9877  fin1a2lem12  10482  catlid  17850  catrid  17851  gsumval2  18868  lbsextlem3  21431  psrbagsn  22365  psdmul  22480  musum  27511  ppiub  27524  umgrupgr  29674  umgrislfupgr  29694  usgruspgr  29754  usgrislfuspgr  29761  disjxwwlksn  30486  wwlksnfi  30488  disjxwwlkn  30495  clwwlknclwwlkdifnum  30564  konigsbergssiedgw  30844  omssubadd  34925  bj-unrab  37819  poimirlem26  38544  poimirlem27  38545  ssrabi  39164  lclkrs2  42577  ovolval5lem3  47633