Theorem ss2abdv 4005

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

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

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 2715  df-ss 3906

This theorem is referenced by:  ss2abi  4006  abssdv  4007  rabss2  4017  intss  4911  ssopab2  5501  ssoprab2  7435  suppimacnvss  8123  suppimacnv  8124  ressuppss  8133  ss2ixp  8858  fiss  9337  tcss  9663  tcel  9664  infmap2  10139  cfub  10171  cflm  10172  cflecard  10175  clsslem  14946  cncmet  25289  plyss  26164  iunrnmptss  32635  ofrn2  32713  sigaclci  34276  subfacp1lem6  35367  ss2mcls  35750  itg2addnclem  37992  sdclem1  38064  istotbnd3  38092  sstotbnd  38096  qsss1  38616  disjdmqscossss  39227  sticksstones4  42588  sticksstones14  42599  sticksstones20  42605  sticksstones22  42607  ssabdv  42661  aomclem4  43485  hbtlem4  43554  hbtlem3  43555  rngunsnply  43597  iocinico  43640