Theorem ss2abdv 4016

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

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

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 2741  df-ss 3919

This theorem is used by:  ss2abi  4017  abssdv  4018  rabss2  4028  intss  4932  ssopab2  5529  ssoprab2  7485  suppimacnvss  8175  suppimacnv  8176  ressuppss  8185  ss2ixp  8921  fiss  9398  tcss  9725  tcel  9726  infmap2  10223  cfub  10254  cflm  10255  cflecard  10258  clsslem  15061  cncmet  25556  plyss  26431  iunrnmptss  33046  ofrn2  33121  sigaclci  34650  subfacp1lem6  35772  ss2mcls  36155  itg2addnclem  38428  sdclem1  38501  istotbnd3  38529  sstotbnd  38533  qsss1  39051  disjdmqscossss  39662  sticksstones4  43023  sticksstones14  43034  sticksstones20  43040  sticksstones22  43042  ssabdv  43098  aomclem4  43906  hbtlem4  43975  hbtlem3  43976  rngunsnply  44018  iocinico  44061