Theorem ss2abdv 4018

Description: Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.) Avoid ax-8 2108, ax-10 2137, ax-11 2154, ax-12 2171. (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 3915	. . 3 ⊢ ({𝑥 ∣ 𝜓} ∩ {𝑥 ∣ 𝜒}) = {𝑦 ∣ (𝑦 ∈ {𝑥 ∣ 𝜓} ∧ 𝑦 ∈ {𝑥 ∣ 𝜒})}
2		df-clab 2714	. . . . . . 7 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜓} ↔ [𝑦 / 𝑥]𝜓)
3	2	bicomi 223	. . . . . 6 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝑦 ∈ {𝑥 ∣ 𝜓})
4		df-clab 2714	. . . . . . 7 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜒} ↔ [𝑦 / 𝑥]𝜒)
5	4	bicomi 223	. . . . . 6 ⊢ ([𝑦 / 𝑥]𝜒 ↔ 𝑦 ∈ {𝑥 ∣ 𝜒})
6	3, 5	anbi12i 627	. . . . 5 ⊢ (([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ (𝑦 ∈ {𝑥 ∣ 𝜓} ∧ 𝑦 ∈ {𝑥 ∣ 𝜒}))
7	6	abbii 2806	. . . 4 ⊢ {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} = {𝑦 ∣ (𝑦 ∈ {𝑥 ∣ 𝜓} ∧ 𝑦 ∈ {𝑥 ∣ 𝜒})}
8		sbequ 2086	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜓 ↔ [𝑧 / 𝑥]𝜓))
9		sbequ 2086	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜒 ↔ [𝑧 / 𝑥]𝜒))
10	8, 9	anbi12d 631	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ ([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒)))
11	10	sbievw 2095	. . . . . . 7 ⊢ ([𝑧 / 𝑦]([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ ([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒))
12		ax-1 6	. . . . . . . . . 10 ⊢ ([𝑧 / 𝑥]𝜓 → ([𝑧 / 𝑥]𝜒 → [𝑧 / 𝑥]𝜓))
13	12	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 → ([𝑧 / 𝑥]𝜒 → [𝑧 / 𝑥]𝜓)))
14	13	impd 411	. . . . . . . 8 ⊢ (𝜑 → (([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒) → [𝑧 / 𝑥]𝜓))
15		ss2abdv.1	. . . . . . . . . 10 ⊢ (𝜑 → (𝜓 → 𝜒))
16	15	sbimdv 2081	. . . . . . . . 9 ⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜒))
17	16	ancld 551	. . . . . . . 8 ⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 → ([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒)))
18	14, 17	impbid 211	. . . . . . 7 ⊢ (𝜑 → (([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒) ↔ [𝑧 / 𝑥]𝜓))
19	11, 18	bitrid 282	. . . . . 6 ⊢ (𝜑 → ([𝑧 / 𝑦]([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ [𝑧 / 𝑥]𝜓))
20		df-clab 2714	. . . . . 6 ⊢ (𝑧 ∈ {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} ↔ [𝑧 / 𝑦]([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒))
21		df-clab 2714	. . . . . 6 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜓} ↔ [𝑧 / 𝑥]𝜓)
22	19, 20, 21	3bitr4g 313	. . . . 5 ⊢ (𝜑 → (𝑧 ∈ {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} ↔ 𝑧 ∈ {𝑥 ∣ 𝜓}))
23	22	eqrdv 2734	. . . 4 ⊢ (𝜑 → {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} = {𝑥 ∣ 𝜓})
24	7, 23	eqtr3id 2790	. . 3 ⊢ (𝜑 → {𝑦 ∣ (𝑦 ∈ {𝑥 ∣ 𝜓} ∧ 𝑦 ∈ {𝑥 ∣ 𝜒})} = {𝑥 ∣ 𝜓})
25	1, 24	eqtrid 2788	. 2 ⊢ (𝜑 → ({𝑥 ∣ 𝜓} ∩ {𝑥 ∣ 𝜒}) = {𝑥 ∣ 𝜓})
26		df-ss 3925	. 2 ⊢ ({𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝜒} ↔ ({𝑥 ∣ 𝜓} ∩ {𝑥 ∣ 𝜒}) = {𝑥 ∣ 𝜓})
27	25, 26	sylibr 233	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝜒})

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541  [wsb 2067   ∈ wcel 2106  {cab 2713   ∩ cin 3907   ⊆ wss 3908

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-in 3915  df-ss 3925

This theorem is referenced by:  ss2abi  4021  abssdv  4023  intss  4928  ssopab2  5501  ssoprab2  7419  suppimacnvss  8096  suppimacnv  8097  ressuppss  8106  ss2ixp  8806  fiss  9318  tcss  9638  tcel  9639  infmap2  10112  cfub  10143  cflm  10144  cflecard  10147  clsslem  14823  cncmet  24632  plyss  25506  iunrnmptss  31329  ofrn2  31401  sigaclci  32559  subfacp1lem6  33607  ss2mcls  33990  itg2addnclem  36061  sdclem1  36134  istotbnd3  36162  sstotbnd  36166  qsss1  36681  disjdmqscossss  37197  sticksstones4  40489  sticksstones14  40500  sticksstones20  40506  sticksstones22  40508  ssabdv  40573  aomclem4  41287  hbtlem4  41356  hbtlem3  41357  rngunsnply  41403  iocinico  41449