Theorem ss2rabi 4030

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 481	. . 3 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐴) → (𝜑 → 𝜓))
3	2	ss2rabdv 4029	. 2 ⊢ (⊤ → {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓})
4	3	mptru 1549	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4  ⊤wtru 1543   ∈ wcel 2114  {crab 3401   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-ral 3053  df-rab 3402  df-ss 3920

This theorem is referenced by:  f1ossf1o  7083  mptexgf  7178  supub  9374  suplub  9375  card2on  9471  rankval4  9791  fin1a2lem12  10333  catlid  17618  catrid  17619  gsumval2  18623  lbsextlem3  21127  psrbagsn  22030  psdmul  22121  musum  27169  ppiub  27183  umgrupgr  29188  umgrislfupgr  29208  usgruspgr  29265  usgrislfuspgr  29272  disjxwwlksn  29989  wwlksnfi  29991  disjxwwlkn  29998  clwwlknclwwlkdifnum  30067  konigsbergssiedgw  30337  omssubadd  34478  bj-unrab  37174  poimirlem26  37897  poimirlem27  37898  ssrabi  38503  lclkrs2  41916  ovolval5lem3  47012