Theorem ss2abdv 4019

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

Syntax hints:   → wi 4  [wsb 2068   ∈ wcel 2114  {cab 2715   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-ss 3920

This theorem is referenced by:  ss2abi  4020  abssdv  4021  rabss2  4031  intss  4926  ssopab2  5502  ssoprab2  7436  suppimacnvss  8125  suppimacnv  8126  ressuppss  8135  ss2ixp  8860  fiss  9339  tcss  9663  tcel  9664  infmap2  10139  cfub  10171  cflm  10172  cflecard  10175  clsslem  14919  cncmet  25290  plyss  26172  iunrnmptss  32651  ofrn2  32729  sigaclci  34309  subfacp1lem6  35398  ss2mcls  35781  itg2addnclem  37919  sdclem1  37991  istotbnd3  38019  sstotbnd  38023  qsss1  38543  disjdmqscossss  39154  sticksstones4  42516  sticksstones14  42527  sticksstones20  42533  sticksstones22  42535  ssabdv  42589  aomclem4  43411  hbtlem4  43480  hbtlem3  43481  rngunsnply  43523  iocinico  43566