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

Syntax hints:   → wi 4  ⊤wtru 1571   ∈ wcel 2143  {crab 3416   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-ral 3080  df-rab 3417  df-ss 3922

This theorem is referenced by:  f1ossf1o  7124  mptexgf  7220  supub  9415  suplub  9416  card2on  9512  rankval4  9835  fin1a2lem12  10390  catlid  17734  catrid  17735  gsumval2  18739  lbsextlem3  21284  psrbagsn  22214  psdmul  22329  musum  27355  ppiub  27368  umgrupgr  29453  umgrislfupgr  29473  usgruspgr  29530  usgrislfuspgr  29537  disjxwwlksn  30253  wwlksnfi  30255  disjxwwlkn  30262  clwwlknclwwlkdifnum  30331  konigsbergssiedgw  30601  omssubadd  34690  bj-unrab  37562  poimirlem26  38297  poimirlem27  38298  ssrabi  38901  lclkrs2  42314  ovolval5lem3  47368