Theorem ss2abdv 4013

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 2115	. . 3 ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜒))
3		df-clab 2740	. . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜓} ↔ [𝑦 / 𝑥]𝜓)
4		df-clab 2740	. . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜒} ↔ [𝑦 / 𝑥]𝜒)
5	2, 3, 4	3imtr4g 299	. 2 ⊢ (𝜑 → (𝑦 ∈ {𝑥 ∣ 𝜓} → 𝑦 ∈ {𝑥 ∣ 𝜒}))
6	5	ssrdv 3937	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝜒})

This proof depends on syntax axioms:   → wi 4  [wsb 2099   ∈ wcel 2145  {cab 2739   ⊆ wss 3899

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

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-ss 3916

This theorem is used by:  ss2abi  4014  abssdv  4015  rabss2  4025  intss  4929  ssopab2  5521  ssoprab2  7480  suppimacnvss  8174  suppimacnv  8175  ressuppss  8184  ss2ixp  8922  fiss  9400  tcss  9727  tcel  9728  infmap2  10276  cfub  10307  cflm  10308  cflecard  10311  clsslem  15117  cncmet  25623  plyss  26497  iunrnmptss  33141  ofrn2  33216  sigaclci  34746  subfacp1lem6  35919  ss2mcls  36302  itg2addnclem  38557  dfprop2  38614  sdclem1  38645  istotbnd3  38673  sstotbnd  38677  qsss1  39195  disjdmqscossss  39806  sticksstones4  43167  sticksstones14  43178  sticksstones20  43184  sticksstones22  43186  ssabdv  43242  aomclem4  44017  hbtlem4  44086  hbtlem3  44087  rngunsnply  44129  iocinico  44172