Theorem ss2abdv 4022

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

This proof depends on syntax axioms:   → wi 4  [wsb 2099   ∈ wcel 2146  {cab 2744   ⊆ wss 3908

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 2745  df-ss 3925

This theorem is used by:  ss2abi  4023  abssdv  4024  rabss2  4034  intss  4939  ssopab2  5536  ssoprab2  7491  suppimacnvss  8178  suppimacnv  8179  ressuppss  8188  ss2ixp  8917  fiss  9394  tcss  9721  tcel  9722  infmap2  10219  cfub  10250  cflm  10251  cflecard  10254  clsslem  15047  cncmet  25518  plyss  26393  iunrnmptss  32947  ofrn2  33022  sigaclci  34553  subfacp1lem6  35698  ss2mcls  36081  itg2addnclem  38363  sdclem1  38435  istotbnd3  38463  sstotbnd  38467  qsss1  38985  disjdmqscossss  39596  sticksstones4  42957  sticksstones14  42968  sticksstones20  42974  sticksstones22  42976  ssabdv  43032  aomclem4  43825  hbtlem4  43894  hbtlem3  43895  rngunsnply  43937  iocinico  43980