Theorem ss2abdv 4020

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

Syntax hints:   → wi 4  [wsb 2096   ∈ wcel 2143  {cab 2741   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-ss 3923

This theorem is referenced by:  ss2abi  4021  abssdv  4022  rabss2  4032  intss  4935  ssopab2  5533  ssoprab2  7480  suppimacnvss  8170  suppimacnv  8171  ressuppss  8180  ss2ixp  8909  fiss  9385  tcss  9712  tcel  9713  infmap2  10201  cfub  10233  cflm  10234  cflecard  10237  clsslem  15023  cncmet  25462  plyss  26337  iunrnmptss  32888  ofrn2  32963  sigaclci  34500  subfacp1lem6  35655  ss2mcls  36038  itg2addnclem  38300  sdclem1  38372  istotbnd3  38400  sstotbnd  38404  qsss1  38922  disjdmqscossss  39533  sticksstones4  42894  sticksstones14  42905  sticksstones20  42911  sticksstones22  42913  ssabdv  42969  aomclem4  43764  hbtlem4  43833  hbtlem3  43834  rngunsnply  43876  iocinico  43919