Theorem ss2rabi 4029

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

Syntax hints:   → wi 4  ⊤wtru 1561   ∈ wcel 2142  {crab 3414   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-ral 3077  df-rab 3415  df-ss 3921

This theorem is referenced by:  f1ossf1o  7110  mptexgf  7206  supub  9405  suplub  9406  card2on  9502  rankval4  9825  fin1a2lem12  10368  catlid  17715  catrid  17716  gsumval2  18720  lbsextlem3  21227  psrbagsn  22113  psdmul  22228  musum  27252  ppiub  27265  umgrupgr  29301  umgrislfupgr  29321  usgruspgr  29378  usgrislfuspgr  29385  disjxwwlksn  30101  wwlksnfi  30103  disjxwwlkn  30110  clwwlknclwwlkdifnum  30179  konigsbergssiedgw  30449  omssubadd  34594  bj-unrab  37408  poimirlem26  38142  poimirlem27  38143  ssrabi  38748  lclkrs2  42161  ovolval5lem3  47225