Theorem ss2rabi 4000

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

This proof depends on syntax axioms:   → wi 4  ⊤wtru 1570   ∈ wcel 2144  {crab 3412   ⊆ wss 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-ral 3077  df-rab 3413  df-ss 3897

This theorem is used by:  f1ossf1o  7134  mptexgf  7232  supub  9458  suplub  9459  card2on  9555  rankval4  9891  fin1a2lem12  10496  catlid  17866  catrid  17867  gsumval2  18884  lbsextlem3  21447  psrbagsn  22381  psdmul  22496  musum  27527  ppiub  27540  umgrupgr  29690  umgrislfupgr  29710  usgruspgr  29770  usgrislfuspgr  29777  disjxwwlksn  30502  wwlksnfi  30504  disjxwwlkn  30511  clwwlknclwwlkdifnum  30580  konigsbergssiedgw  30860  omssubadd  34982  rankse  35797  bj-unrab  37935  poimirlem26  38673  poimirlem27  38674  ssrabi  39293  lclkrs2  42706  ovolval5lem3  47772