Theorem ss2abdv 4066

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

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

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 2715  df-ss 3968

This theorem is referenced by:  ss2abi  4067  abssdv  4068  intss  4969  ssopab2  5551  ssoprab2  7501  suppimacnvss  8198  suppimacnv  8199  ressuppss  8208  ss2ixp  8950  fiss  9464  tcss  9784  tcel  9785  infmap2  10257  cfub  10289  cflm  10290  cflecard  10293  clsslem  15023  cncmet  25356  plyss  26238  iunrnmptss  32578  ofrn2  32650  sigaclci  34133  subfacp1lem6  35190  ss2mcls  35573  itg2addnclem  37678  sdclem1  37750  istotbnd3  37778  sstotbnd  37782  qsss1  38290  disjdmqscossss  38804  sticksstones4  42150  sticksstones14  42161  sticksstones20  42167  sticksstones22  42169  ssabdv  42259  aomclem4  43069  hbtlem4  43138  hbtlem3  43139  rngunsnply  43181  iocinico  43224