Theorem ss2abdv 4059

Description: Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.) Avoid ax-8 2106, ax-10 2135, ax-11 2152, ax-12 2169. (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 3954	. . 3 ⊢ ({𝑥 ∣ 𝜓} ∩ {𝑥 ∣ 𝜒}) = {𝑦 ∣ (𝑦 ∈ {𝑥 ∣ 𝜓} ∧ 𝑦 ∈ {𝑥 ∣ 𝜒})}
2		df-clab 2708	. . . . . . 7 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜓} ↔ [𝑦 / 𝑥]𝜓)
3	2	bicomi 223	. . . . . 6 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝑦 ∈ {𝑥 ∣ 𝜓})
4		df-clab 2708	. . . . . . 7 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜒} ↔ [𝑦 / 𝑥]𝜒)
5	4	bicomi 223	. . . . . 6 ⊢ ([𝑦 / 𝑥]𝜒 ↔ 𝑦 ∈ {𝑥 ∣ 𝜒})
6	3, 5	anbi12i 625	. . . . 5 ⊢ (([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ (𝑦 ∈ {𝑥 ∣ 𝜓} ∧ 𝑦 ∈ {𝑥 ∣ 𝜒}))
7	6	abbii 2800	. . . 4 ⊢ {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} = {𝑦 ∣ (𝑦 ∈ {𝑥 ∣ 𝜓} ∧ 𝑦 ∈ {𝑥 ∣ 𝜒})}
8		sbequ 2084	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜓 ↔ [𝑧 / 𝑥]𝜓))
9		sbequ 2084	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜒 ↔ [𝑧 / 𝑥]𝜒))
10	8, 9	anbi12d 629	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ ([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒)))
11	10	sbievw 2093	. . . . . . 7 ⊢ ([𝑧 / 𝑦]([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ ([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒))
12		ax-1 6	. . . . . . . . . 10 ⊢ ([𝑧 / 𝑥]𝜓 → ([𝑧 / 𝑥]𝜒 → [𝑧 / 𝑥]𝜓))
13	12	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 → ([𝑧 / 𝑥]𝜒 → [𝑧 / 𝑥]𝜓)))
14	13	impd 409	. . . . . . . 8 ⊢ (𝜑 → (([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒) → [𝑧 / 𝑥]𝜓))
15		ss2abdv.1	. . . . . . . . . 10 ⊢ (𝜑 → (𝜓 → 𝜒))
16	15	sbimdv 2079	. . . . . . . . 9 ⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜒))
17	16	ancld 549	. . . . . . . 8 ⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 → ([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒)))
18	14, 17	impbid 211	. . . . . . 7 ⊢ (𝜑 → (([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒) ↔ [𝑧 / 𝑥]𝜓))
19	11, 18	bitrid 282	. . . . . 6 ⊢ (𝜑 → ([𝑧 / 𝑦]([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ [𝑧 / 𝑥]𝜓))
20		df-clab 2708	. . . . . 6 ⊢ (𝑧 ∈ {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} ↔ [𝑧 / 𝑦]([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒))
21		df-clab 2708	. . . . . 6 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜓} ↔ [𝑧 / 𝑥]𝜓)
22	19, 20, 21	3bitr4g 313	. . . . 5 ⊢ (𝜑 → (𝑧 ∈ {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} ↔ 𝑧 ∈ {𝑥 ∣ 𝜓}))
23	22	eqrdv 2728	. . . 4 ⊢ (𝜑 → {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} = {𝑥 ∣ 𝜓})
24	7, 23	eqtr3id 2784	. . 3 ⊢ (𝜑 → {𝑦 ∣ (𝑦 ∈ {𝑥 ∣ 𝜓} ∧ 𝑦 ∈ {𝑥 ∣ 𝜒})} = {𝑥 ∣ 𝜓})
25	1, 24	eqtrid 2782	. 2 ⊢ (𝜑 → ({𝑥 ∣ 𝜓} ∩ {𝑥 ∣ 𝜒}) = {𝑥 ∣ 𝜓})
26		df-ss 3964	. 2 ⊢ ({𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝜒} ↔ ({𝑥 ∣ 𝜓} ∩ {𝑥 ∣ 𝜒}) = {𝑥 ∣ 𝜓})
27	25, 26	sylibr 233	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝜒})

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1539  [wsb 2065   ∈ wcel 2104  {cab 2707   ∩ cin 3946   ⊆ wss 3947

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-in 3954  df-ss 3964

This theorem is referenced by:  ss2abi  4062  abssdv  4064  intss  4972  ssopab2  5545  ssoprab2  7479  suppimacnvss  8160  suppimacnv  8161  ressuppss  8170  ss2ixp  8906  fiss  9421  tcss  9741  tcel  9742  infmap2  10215  cfub  10246  cflm  10247  cflecard  10250  clsslem  14935  cncmet  25070  plyss  25948  iunrnmptss  32064  ofrn2  32132  sigaclci  33428  subfacp1lem6  34474  ss2mcls  34857  itg2addnclem  36842  sdclem1  36914  istotbnd3  36942  sstotbnd  36946  qsss1  37460  disjdmqscossss  37976  sticksstones4  41271  sticksstones14  41282  sticksstones20  41288  sticksstones22  41290  ssabdv  41343  aomclem4  42101  hbtlem4  42170  hbtlem3  42171  rngunsnply  42217  iocinico  42263