Theorem ss2rabi 4028

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-ral 3052  df-rab 3400  df-ss 3918

This theorem is referenced by:  f1ossf1o  7073  mptexgf  7168  supub  9362  suplub  9363  card2on  9459  rankval4  9779  fin1a2lem12  10321  catlid  17606  catrid  17607  gsumval2  18611  lbsextlem3  21115  psrbagsn  22018  psdmul  22109  musum  27157  ppiub  27171  umgrupgr  29176  umgrislfupgr  29196  usgruspgr  29253  usgrislfuspgr  29260  disjxwwlksn  29977  wwlksnfi  29979  disjxwwlkn  29986  clwwlknclwwlkdifnum  30055  konigsbergssiedgw  30325  omssubadd  34457  bj-unrab  37127  poimirlem26  37847  poimirlem27  37848  ssrabi  38448  lclkrs2  41800  ovolval5lem3  46898