Theorem ss2abdv 4003

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

Syntax hints:   → wi 4  [wsb 2073   ∈ wcel 2119  {cab 2718   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-ss 3907

This theorem is referenced by:  ss2abi  4004  abssdv  4005  rabss2  4015  intss  4906  ssopab2  5495  ssoprab2  7431  suppimacnvss  8120  suppimacnv  8121  ressuppss  8130  ss2ixp  8855  fiss  9334  tcss  9661  tcel  9662  infmap2  10137  cfub  10169  cflm  10170  cflecard  10173  clsslem  14944  cncmet  25314  plyss  26189  iunrnmptss  32661  ofrn2  32739  sigaclci  34323  subfacp1lem6  35420  ss2mcls  35803  itg2addnclem  38045  sdclem1  38117  istotbnd3  38145  sstotbnd  38149  qsss1  38669  disjdmqscossss  39280  sticksstones4  42641  sticksstones14  42652  sticksstones20  42658  sticksstones22  42660  ssabdv  42714  aomclem4  43509  hbtlem4  43578  hbtlem3  43579  rngunsnply  43621  iocinico  43664