Theorem ss2abdv 4006

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

Syntax hints:   → wi 4  [wsb 2068   ∈ wcel 2114  {cab 2715   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-ss 3907

This theorem is referenced by:  ss2abi  4007  abssdv  4008  rabss2  4018  intss  4912  ssopab2  5494  ssoprab2  7428  suppimacnvss  8116  suppimacnv  8117  ressuppss  8126  ss2ixp  8851  fiss  9330  tcss  9654  tcel  9655  infmap2  10130  cfub  10162  cflm  10163  cflecard  10166  clsslem  14937  cncmet  25299  plyss  26174  iunrnmptss  32650  ofrn2  32728  sigaclci  34292  subfacp1lem6  35383  ss2mcls  35766  itg2addnclem  38006  sdclem1  38078  istotbnd3  38106  sstotbnd  38110  qsss1  38630  disjdmqscossss  39241  sticksstones4  42602  sticksstones14  42613  sticksstones20  42619  sticksstones22  42621  ssabdv  42675  aomclem4  43503  hbtlem4  43572  hbtlem3  43573  rngunsnply  43615  iocinico  43658