Theorem ss2abdv 4014

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

Syntax hints:   → wi 4  [wsb 2067   ∈ wcel 2113  {cab 2711   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-ss 3915

This theorem is referenced by:  ss2abi  4015  abssdv  4016  rabss2  4026  intss  4921  ssopab2  5491  ssoprab2  7422  suppimacnvss  8111  suppimacnv  8112  ressuppss  8121  ss2ixp  8842  fiss  9317  tcss  9641  tcel  9642  infmap2  10117  cfub  10149  cflm  10150  cflecard  10153  clsslem  14895  cncmet  25252  plyss  26134  iunrnmptss  32549  ofrn2  32626  sigaclci  34168  subfacp1lem6  35252  ss2mcls  35635  itg2addnclem  37734  sdclem1  37806  istotbnd3  37834  sstotbnd  37838  qsss1  38350  disjdmqscossss  38924  sticksstones4  42265  sticksstones14  42276  sticksstones20  42282  sticksstones22  42284  ssabdv  42341  aomclem4  43177  hbtlem4  43246  hbtlem3  43247  rngunsnply  43289  iocinico  43332