Theorem ss2abdv 4041

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

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

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 2065  df-clab 2714  df-ss 3943

This theorem is referenced by:  ss2abi  4042  abssdv  4043  intss  4945  ssopab2  5521  ssoprab2  7475  suppimacnvss  8172  suppimacnv  8173  ressuppss  8182  ss2ixp  8924  fiss  9436  tcss  9758  tcel  9759  infmap2  10231  cfub  10263  cflm  10264  cflecard  10267  clsslem  15003  cncmet  25274  plyss  26156  iunrnmptss  32546  ofrn2  32618  sigaclci  34163  subfacp1lem6  35207  ss2mcls  35590  itg2addnclem  37695  sdclem1  37767  istotbnd3  37795  sstotbnd  37799  qsss1  38307  disjdmqscossss  38821  sticksstones4  42162  sticksstones14  42173  sticksstones20  42179  sticksstones22  42181  ssabdv  42271  aomclem4  43081  hbtlem4  43150  hbtlem3  43151  rngunsnply  43193  iocinico  43236