Theorem ss2abdv 4029

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

Syntax hints:   → wi 4  [wsb 2065   ∈ wcel 2109  {cab 2707   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-sb 2066  df-clab 2708  df-ss 3931

This theorem is referenced by:  ss2abi  4030  abssdv  4031  intss  4933  ssopab2  5506  ssoprab2  7457  suppimacnvss  8152  suppimacnv  8153  ressuppss  8162  ss2ixp  8883  fiss  9375  tcss  9697  tcel  9698  infmap2  10170  cfub  10202  cflm  10203  cflecard  10206  clsslem  14950  cncmet  25222  plyss  26104  iunrnmptss  32494  ofrn2  32564  sigaclci  34122  subfacp1lem6  35172  ss2mcls  35555  itg2addnclem  37665  sdclem1  37737  istotbnd3  37765  sstotbnd  37769  qsss1  38277  disjdmqscossss  38795  sticksstones4  42137  sticksstones14  42148  sticksstones20  42154  sticksstones22  42156  ssabdv  42208  aomclem4  43046  hbtlem4  43115  hbtlem3  43116  rngunsnply  43158  iocinico  43201