Theorem ss2abdv 3977

Description: Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.) Avoid ax-8 2112, ax-10 2141, ax-11 2158, ax-12 2175. (Revised by Gino Giotto, 28-Jun-2024.)

Hypothesis

Ref	Expression
ss2abdv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
ss2abdv	⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝜒})

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem ss2abdv

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-in 3873	. . 3 ⊢ ({𝑥 ∣ 𝜓} ∩ {𝑥 ∣ 𝜒}) = {𝑦 ∣ (𝑦 ∈ {𝑥 ∣ 𝜓} ∧ 𝑦 ∈ {𝑥 ∣ 𝜒})}
2		df-clab 2715	. . . . . . 7 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜓} ↔ [𝑦 / 𝑥]𝜓)
3	2	bicomi 227	. . . . . 6 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝑦 ∈ {𝑥 ∣ 𝜓})
4		df-clab 2715	. . . . . . 7 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜒} ↔ [𝑦 / 𝑥]𝜒)
5	4	bicomi 227	. . . . . 6 ⊢ ([𝑦 / 𝑥]𝜒 ↔ 𝑦 ∈ {𝑥 ∣ 𝜒})
6	3, 5	anbi12i 630	. . . . 5 ⊢ (([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ (𝑦 ∈ {𝑥 ∣ 𝜓} ∧ 𝑦 ∈ {𝑥 ∣ 𝜒}))
7	6	abbii 2808	. . . 4 ⊢ {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} = {𝑦 ∣ (𝑦 ∈ {𝑥 ∣ 𝜓} ∧ 𝑦 ∈ {𝑥 ∣ 𝜒})}
8		sbequ 2089	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜓 ↔ [𝑧 / 𝑥]𝜓))
9		sbequ 2089	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜒 ↔ [𝑧 / 𝑥]𝜒))
10	8, 9	anbi12d 634	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ ([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒)))
11	10	sbievw 2099	. . . . . . 7 ⊢ ([𝑧 / 𝑦]([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ ([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒))
12		ax-1 6	. . . . . . . . . 10 ⊢ ([𝑧 / 𝑥]𝜓 → ([𝑧 / 𝑥]𝜒 → [𝑧 / 𝑥]𝜓))
13	12	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 → ([𝑧 / 𝑥]𝜒 → [𝑧 / 𝑥]𝜓)))
14	13	impd 414	. . . . . . . 8 ⊢ (𝜑 → (([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒) → [𝑧 / 𝑥]𝜓))
15		ss2abdv.1	. . . . . . . . . 10 ⊢ (𝜑 → (𝜓 → 𝜒))
16	15	sbimdv 2084	. . . . . . . . 9 ⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜒))
17	16	ancld 554	. . . . . . . 8 ⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 → ([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒)))
18	14, 17	impbid 215	. . . . . . 7 ⊢ (𝜑 → (([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒) ↔ [𝑧 / 𝑥]𝜓))
19	11, 18	syl5bb 286	. . . . . 6 ⊢ (𝜑 → ([𝑧 / 𝑦]([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ [𝑧 / 𝑥]𝜓))
20		df-clab 2715	. . . . . 6 ⊢ (𝑧 ∈ {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} ↔ [𝑧 / 𝑦]([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒))
21		df-clab 2715	. . . . . 6 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜓} ↔ [𝑧 / 𝑥]𝜓)
22	19, 20, 21	3bitr4g 317	. . . . 5 ⊢ (𝜑 → (𝑧 ∈ {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} ↔ 𝑧 ∈ {𝑥 ∣ 𝜓}))
23	22	eqrdv 2735	. . . 4 ⊢ (𝜑 → {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} = {𝑥 ∣ 𝜓})
24	7, 23	eqtr3id 2792	. . 3 ⊢ (𝜑 → {𝑦 ∣ (𝑦 ∈ {𝑥 ∣ 𝜓} ∧ 𝑦 ∈ {𝑥 ∣ 𝜒})} = {𝑥 ∣ 𝜓})
25	1, 24	eqtrid 2789	. 2 ⊢ (𝜑 → ({𝑥 ∣ 𝜓} ∩ {𝑥 ∣ 𝜒}) = {𝑥 ∣ 𝜓})
26		df-ss 3883	. 2 ⊢ ({𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝜒} ↔ ({𝑥 ∣ 𝜓} ∩ {𝑥 ∣ 𝜒}) = {𝑥 ∣ 𝜓})
27	25, 26	sylibr 237	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝜒})

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543  [wsb 2070   ∈ wcel 2110  {cab 2714   ∩ cin 3865   ⊆ wss 3866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-in 3873  df-ss 3883

This theorem is referenced by:  ss2abi  3980  intss  4880  ssopab2  5427  ssoprab2  7279  suppimacnvss  7915  suppimacnv  7916  ressuppss  7925  ss2ixp  8591  fiss  9040  tcss  9360  tcel  9361  infmap2  9832  cfub  9863  cflm  9864  cflecard  9867  clsslem  14547  cncmet  24219  plyss  25093  iunrnmptss  30624  ofrn2  30696  sigaclci  31812  subfacp1lem6  32860  ss2mcls  33243  itg2addnclem  35565  sdclem1  35638  istotbnd3  35666  sstotbnd  35670  qsss1  36160  sticksstones4  39827  sticksstones14  39838  sticksstones20  39844  sticksstones22  39846  aomclem4  40585  hbtlem4  40654  hbtlem3  40655  rngunsnply  40701  iocinico  40746