Theorem ss2abdv 4089

Description: Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.) (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 2078	. . 3 ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜒))
3		df-clab 2718	. . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜓} ↔ [𝑦 / 𝑥]𝜓)
4		df-clab 2718	. . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜒} ↔ [𝑦 / 𝑥]𝜒)
5	2, 3, 4	3imtr4g 296	. 2 ⊢ (𝜑 → (𝑦 ∈ {𝑥 ∣ 𝜓} → 𝑦 ∈ {𝑥 ∣ 𝜒}))
6	5	ssrdv 4014	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝜒})

Syntax hints:   → wi 4  [wsb 2064   ∈ wcel 2108  {cab 2717   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-sb 2065  df-clab 2718  df-ss 3993

This theorem is referenced by:  ss2abi  4090  abssdv  4091  intss  4993  ssopab2  5565  ssoprab2  7518  suppimacnvss  8214  suppimacnv  8215  ressuppss  8224  ss2ixp  8968  fiss  9493  tcss  9813  tcel  9814  infmap2  10286  cfub  10318  cflm  10319  cflecard  10322  clsslem  15033  cncmet  25375  plyss  26258  iunrnmptss  32588  ofrn2  32659  sigaclci  34096  subfacp1lem6  35153  ss2mcls  35536  itg2addnclem  37631  sdclem1  37703  istotbnd3  37731  sstotbnd  37735  qsss1  38245  disjdmqscossss  38759  sticksstones4  42106  sticksstones14  42117  sticksstones20  42123  sticksstones22  42125  ssabdv  42213  aomclem4  43014  hbtlem4  43083  hbtlem3  43084  rngunsnply  43130  iocinico  43173