Theorem ss2abdv 4020

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

Syntax hints:   → wi 4  [wsb 2065   ∈ wcel 2109  {cab 2707   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-sb 2066  df-clab 2708  df-ss 3922

This theorem is referenced by:  ss2abi  4021  abssdv  4022  intss  4922  ssopab2  5493  ssoprab2  7421  suppimacnvss  8113  suppimacnv  8114  ressuppss  8123  ss2ixp  8844  fiss  9333  tcss  9659  tcel  9660  infmap2  10130  cfub  10162  cflm  10163  cflecard  10166  clsslem  14909  cncmet  25238  plyss  26120  iunrnmptss  32527  ofrn2  32597  sigaclci  34101  subfacp1lem6  35160  ss2mcls  35543  itg2addnclem  37653  sdclem1  37725  istotbnd3  37753  sstotbnd  37757  qsss1  38265  disjdmqscossss  38783  sticksstones4  42125  sticksstones14  42136  sticksstones20  42142  sticksstones22  42144  ssabdv  42196  aomclem4  43033  hbtlem4  43102  hbtlem3  43103  rngunsnply  43145  iocinico  43188