Theorem ss2rabi 4017

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

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

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 3391  df-ss 3907

This theorem is referenced by:  f1ossf1o  7076  mptexgf  7171  supub  9366  suplub  9367  card2on  9463  rankval4  9785  fin1a2lem12  10327  catlid  17643  catrid  17644  gsumval2  18648  lbsextlem3  21153  psrbagsn  22054  psdmul  22145  musum  27171  ppiub  27184  umgrupgr  29189  umgrislfupgr  29209  usgruspgr  29266  usgrislfuspgr  29273  disjxwwlksn  29990  wwlksnfi  29992  disjxwwlkn  29999  clwwlknclwwlkdifnum  30068  konigsbergssiedgw  30338  omssubadd  34463  bj-unrab  37252  poimirlem26  37984  poimirlem27  37985  ssrabi  38590  lclkrs2  42003  ovolval5lem3  47103