Theorem ss2abdv 4032

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

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

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 2709  df-ss 3934

This theorem is referenced by:  ss2abi  4033  abssdv  4034  intss  4936  ssopab2  5509  ssoprab2  7460  suppimacnvss  8155  suppimacnv  8156  ressuppss  8165  ss2ixp  8886  fiss  9382  tcss  9704  tcel  9705  infmap2  10177  cfub  10209  cflm  10210  cflecard  10213  clsslem  14957  cncmet  25229  plyss  26111  iunrnmptss  32501  ofrn2  32571  sigaclci  34129  subfacp1lem6  35179  ss2mcls  35562  itg2addnclem  37672  sdclem1  37744  istotbnd3  37772  sstotbnd  37776  qsss1  38284  disjdmqscossss  38802  sticksstones4  42144  sticksstones14  42155  sticksstones20  42161  sticksstones22  42163  ssabdv  42215  aomclem4  43053  hbtlem4  43122  hbtlem3  43123  rngunsnply  43165  iocinico  43208