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  7127  mptexgf  7223  supub  9421  suplub  9422  card2on  9518  rankval4  9841  fin1a2lem12  10397  catlid  17741  catrid  17742  gsumval2  18746  lbsextlem3  21264  psrbagsn  22185  psdmul  22300  musum  27323  ppiub  27336  umgrupgr  29396  umgrislfupgr  29416  usgruspgr  29473  usgrislfuspgr  29480  disjxwwlksn  30196  wwlksnfi  30198  disjxwwlkn  30205  clwwlknclwwlkdifnum  30274  konigsbergssiedgw  30544  omssubadd  34637  bj-unrab  37487  poimirlem26  38222  poimirlem27  38223  ssrabi  38828  lclkrs2  42241  ovolval5lem3  47297