Theorem ss2rabi 4038

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

Syntax hints:   → wi 4  ⊤wtru 1568   ∈ wcel 2149  {crab 3423   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-ral 3086  df-rab 3424  df-ss 3930

This theorem is referenced by:  f1ossf1o  7125  mptexgf  7221  supub  9418  suplub  9419  card2on  9515  rankval4  9838  fin1a2lem12  10394  catlid  17738  catrid  17739  gsumval2  18743  lbsextlem3  21261  psrbagsn  22182  psdmul  22297  musum  27320  ppiub  27333  umgrupgr  29393  umgrislfupgr  29413  usgruspgr  29470  usgrislfuspgr  29477  disjxwwlksn  30193  wwlksnfi  30195  disjxwwlkn  30202  clwwlknclwwlkdifnum  30271  konigsbergssiedgw  30541  omssubadd  34634  bj-unrab  37449  poimirlem26  38184  poimirlem27  38185  ssrabi  38790  lclkrs2  42203  ovolval5lem3  47259