Theorem ss2abdv 4017

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

Syntax hints:   → wi 4  [wsb 2067   ∈ wcel 2111  {cab 2709   ⊆ wss 3902

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

This theorem depends on definitions:  df-bi 207  df-sb 2068  df-clab 2710  df-ss 3919

This theorem is referenced by:  ss2abi  4018  abssdv  4019  intss  4919  ssopab2  5486  ssoprab2  7414  suppimacnvss  8103  suppimacnv  8104  ressuppss  8113  ss2ixp  8834  fiss  9308  tcss  9632  tcel  9633  infmap2  10108  cfub  10140  cflm  10141  cflecard  10144  clsslem  14891  cncmet  25250  plyss  26132  iunrnmptss  32543  ofrn2  32620  sigaclci  34143  subfacp1lem6  35227  ss2mcls  35610  itg2addnclem  37717  sdclem1  37789  istotbnd3  37817  sstotbnd  37821  qsss1  38329  disjdmqscossss  38847  sticksstones4  42188  sticksstones14  42199  sticksstones20  42205  sticksstones22  42207  ssabdv  42259  aomclem4  43096  hbtlem4  43165  hbtlem3  43166  rngunsnply  43208  iocinico  43251