Theorem ss2abdv 3990

Description: Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 28-Jun-2024.)

Hypothesis

Ref	Expression
ss2abdv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
ss2abdv	⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝜒})

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem ss2abdv

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ss2abdv.1	. . . 4 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	sbimdv 2114	. . 3 ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜒))
3		df-clab 2739	. . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜓} ↔ [𝑦 / 𝑥]𝜓)
4		df-clab 2739	. . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜒} ↔ [𝑦 / 𝑥]𝜒)
5	2, 3, 4	3imtr4g 299	. 2 ⊢ (𝜑 → (𝑦 ∈ {𝑥 ∣ 𝜓} → 𝑦 ∈ {𝑥 ∣ 𝜒}))
6	5	ssrdv 3914	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝜒})

This proof depends on syntax axioms:   → wi 4  [wsb 2098   ∈ wcel 2144  {cab 2738   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-ss 3896

This theorem is used by:  ss2abi  3991  abssdv  3992  rabss2  4002  intss  4928  ssopab2  5520  ssoprab2  7488  suppimacnvss  8193  suppimacnv  8194  ressuppss  8203  ss2ixp  8941  fiss  9419  tcss  9746  tcel  9747  infmap2  10298  cfub  10329  cflm  10330  cflecard  10333  clsslem  15142  cncmet  25648  plyss  26522  iunrnmptss  33206  ofrn2  33281  sigaclci  34810  subfacp1lem6  36036  ss2mcls  36419  itg2addnclem  38682  dfprop2  38739  sdclem1  38770  istotbnd3  38798  sstotbnd  38802  qsss1  39320  disjdmqscossss  39931  sticksstones4  43292  sticksstones14  43303  sticksstones20  43309  sticksstones22  43311  ssabdv  43367  aomclem4  44152  hbtlem4  44221  hbtlem3  44222  rngunsnply  44264  iocinico  44307