Theorem ss2abdv 4017

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

Syntax hints:   → wi 4  [wsb 2067   ∈ wcel 2113  {cab 2714   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-ss 3918

This theorem is referenced by:  ss2abi  4018  abssdv  4019  rabss2  4029  intss  4924  ssopab2  5494  ssoprab2  7426  suppimacnvss  8115  suppimacnv  8116  ressuppss  8125  ss2ixp  8848  fiss  9327  tcss  9651  tcel  9652  infmap2  10127  cfub  10159  cflm  10160  cflecard  10163  clsslem  14907  cncmet  25278  plyss  26160  iunrnmptss  32640  ofrn2  32718  sigaclci  34289  subfacp1lem6  35379  ss2mcls  35762  itg2addnclem  37872  sdclem1  37944  istotbnd3  37972  sstotbnd  37976  qsss1  38488  disjdmqscossss  39062  sticksstones4  42403  sticksstones14  42414  sticksstones20  42420  sticksstones22  42422  ssabdv  42476  aomclem4  43299  hbtlem4  43368  hbtlem3  43369  rngunsnply  43411  iocinico  43454