Theorem ss2rabi 4004

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

This proof depends on syntax axioms:   → wi 4  ⊤wtru 1571   ∈ wcel 2147  {crab 3416   ⊆ wss 3900

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-ral 3081  df-rab 3417  df-ss 3901

This theorem is used by:  f1ossf1o  7161  mptexgf  7259  supub  9488  suplub  9489  card2on  9585  rankval4  9921  fin1a2lem12  10528  catlid  17907  catrid  17908  gsumval2  18925  lbsextlem3  21489  psrbagsn  22427  psdmul  22542  musum  27575  ppiub  27588  umgrupgr  29738  umgrislfupgr  29758  usgruspgr  29818  usgrislfuspgr  29825  disjxwwlksn  30550  wwlksnfi  30552  disjxwwlkn  30559  clwwlknclwwlkdifnum  30628  konigsbergssiedgw  30908  omssubadd  35043  rankse  35864  bj-unrab  38054  poimirlem26  38832  poimirlem27  38833  ssrabi  39450  lclkrs2  42863  ovolval5lem3  47937