Theorem ss2rabi 4007

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

Syntax hints:   → wi 4  ⊤wtru 1548   ∈ wcel 2119  {crab 3391   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-ral 3054  df-rab 3392  df-ss 3900

This theorem is referenced by:  f1ossf1o  7070  mptexgf  7166  supub  9362  suplub  9363  card2on  9459  rankval4  9782  fin1a2lem12  10324  catlid  17640  catrid  17641  gsumval2  18645  lbsextlem3  21153  psrbagsn  22039  psdmul  22154  musum  27172  ppiub  27185  umgrupgr  29190  umgrislfupgr  29210  usgruspgr  29267  usgrislfuspgr  29274  disjxwwlksn  29990  wwlksnfi  29992  disjxwwlkn  29999  clwwlknclwwlkdifnum  30068  konigsbergssiedgw  30338  omssubadd  34484  bj-unrab  37279  poimirlem26  38013  poimirlem27  38014  ssrabi  38619  lclkrs2  42032  ovolval5lem3  47097