Theorem ss2rabi 4031

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

This proof depends on syntax axioms:   → wi 4  ⊤wtru 1571   ∈ wcel 2146  {crab 3418   ⊆ wss 3906

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 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-ral 3082  df-rab 3419  df-ss 3923

This theorem is used by:  f1ossf1o  7128  mptexgf  7227  supub  9426  suplub  9427  card2on  9523  rankval4  9846  fin1a2lem12  10410  catlid  17761  catrid  17762  gsumval2  18776  lbsextlem3  21334  psrbagsn  22264  psdmul  22379  musum  27406  ppiub  27419  umgrupgr  29508  umgrislfupgr  29528  usgruspgr  29588  usgrislfuspgr  29595  disjxwwlksn  30320  wwlksnfi  30322  disjxwwlkn  30329  clwwlknclwwlkdifnum  30398  konigsbergssiedgw  30672  omssubadd  34755  bj-unrab  37619  poimirlem26  38354  poimirlem27  38355  ssrabi  38959  lclkrs2  42372  ovolval5lem3  47426