Theorem ss2rabi 4024

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

This proof depends on syntax axioms:   → wi 4  ⊤wtru 1571   ∈ wcel 2145  {crab 3412   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-ral 3077  df-rab 3413  df-ss 3916

This theorem is used by:  f1ossf1o  7122  mptexgf  7221  supub  9429  suplub  9430  card2on  9526  rankval4  9849  fin1a2lem12  10413  catlid  17771  catrid  17772  gsumval2  18788  lbsextlem3  21347  psrbagsn  22279  psdmul  22394  musum  27427  ppiub  27440  umgrupgr  29560  umgrislfupgr  29580  usgruspgr  29640  usgrislfuspgr  29647  disjxwwlksn  30372  wwlksnfi  30374  disjxwwlkn  30381  clwwlknclwwlkdifnum  30450  konigsbergssiedgw  30730  omssubadd  34811  bj-unrab  37670  poimirlem26  38395  poimirlem27  38396  ssrabi  39000  lclkrs2  42413  ovolval5lem3  47482