Theorem ss2abdv 4021

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

Syntax hints:   → wi 4  [wsb 2093   ∈ wcel 2145  {cab 2743   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933

This theorem depends on definitions:  df-bi 210  df-an 401  df-sb 2094  df-clab 2744  df-ss 3924

This theorem is referenced by:  ss2abi  4022  abssdv  4023  rabss2  4033  intss  4930  ssopab2  5522  ssoprab2  7468  suppimacnvss  8157  suppimacnv  8158  ressuppss  8167  ss2ixp  8896  fiss  9372  tcss  9699  tcel  9700  infmap2  10188  cfub  10220  cflm  10221  cflecard  10224  clsslem  15011  cncmet  25442  plyss  26317  iunrnmptss  32820  ofrn2  32897  sigaclci  34439  subfacp1lem6  35548  ss2mcls  35931  itg2addnclem  38182  sdclem1  38254  istotbnd3  38282  sstotbnd  38286  qsss1  38806  disjdmqscossss  39417  sticksstones4  42778  sticksstones14  42789  sticksstones20  42795  sticksstones22  42797  ssabdv  42851  aomclem4  43646  hbtlem4  43715  hbtlem3  43716  rngunsnply  43758  iocinico  43801