Theorem ss2rabi 4026

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

Syntax hints:   → wi 4  ⊤wtru 1542   ∈ wcel 2113  {crab 3397   ⊆ wss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-ral 3050  df-rab 3398  df-ss 3916

This theorem is referenced by:  f1ossf1o  7071  mptexgf  7166  supub  9360  suplub  9361  card2on  9457  rankval4  9777  fin1a2lem12  10319  catlid  17604  catrid  17605  gsumval2  18609  lbsextlem3  21113  psrbagsn  22016  psdmul  22107  musum  27155  ppiub  27169  umgrupgr  29125  umgrislfupgr  29145  usgruspgr  29202  usgrislfuspgr  29209  disjxwwlksn  29926  wwlksnfi  29928  disjxwwlkn  29935  clwwlknclwwlkdifnum  30004  konigsbergssiedgw  30274  omssubadd  34406  bj-unrab  37070  poimirlem26  37786  poimirlem27  37787  ssrabi  38387  lclkrs2  41739  ovolval5lem3  46840