Theorem ss2abdv 3993

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

This proof depends on syntax axioms:   → wi 4  [wsb 2101   ∈ wcel 2147  {cab 2741   ⊆ wss 3900

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 1945  ax-6 2002  ax-7 2043

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-ss 3901

This theorem is used by:  ss2abi  3994  abssdv  3995  rabss2  4005  intss  4932  ssopab2  5526  ssoprab2  7514  suppimacnvss  8221  suppimacnv  8222  ressuppss  8231  ss2ixp  8969  fiss  9446  tcss  9773  tcel  9774  infmap2  10325  cfub  10356  cflm  10357  cflecard  10360  clsslem  15169  cncmet  25676  plyss  26550  iunrnmptss  33234  ofrn2  33309  sigaclci  34847  subfacp1lem6  36130  ss2mcls  36513  itg2addnclem  38794  dfprop2  38851  sdclem1  38880  istotbnd3  38908  sstotbnd  38912  qsss1  39430  disjdmqscossss  40041  sticksstones4  43402  sticksstones14  43413  sticksstones20  43419  sticksstones22  43421  ssabdv  43478  aomclem4  44263  hbtlem4  44331  hbtlem3  44332  rngunsnply  44374  iocinico  44417