Theorem ss2abdv 4018

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

Syntax hints:   → wi 4  [wsb 2089   ∈ wcel 2141  {cab 2739   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-an 400  df-sb 2090  df-clab 2740  df-ss 3921

This theorem is referenced by:  ss2abi  4019  abssdv  4020  rabss2  4030  intss  4926  ssopab2  5515  ssoprab2  7460  suppimacnvss  8148  suppimacnv  8149  ressuppss  8158  ss2ixp  8888  fiss  9367  tcss  9694  tcel  9695  infmap2  10170  cfub  10202  cflm  10203  cflecard  10206  clsslem  14994  cncmet  25364  plyss  26239  iunrnmptss  32714  ofrn2  32792  sigaclci  34390  subfacp1lem6  35499  ss2mcls  35882  itg2addnclem  38134  sdclem1  38206  istotbnd3  38234  sstotbnd  38238  qsss1  38758  disjdmqscossss  39369  sticksstones4  42730  sticksstones14  42741  sticksstones20  42747  sticksstones22  42749  ssabdv  42803  aomclem4  43598  hbtlem4  43667  hbtlem3  43668  rngunsnply  43710  iocinico  43753