Theorem ss2abdv 4001

Description: Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.) Avoid ax-8 2111, ax-10 2140, ax-11 2157, ax-12 2174. (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 3898	. . 3 ⊢ ({𝑥 ∣ 𝜓} ∩ {𝑥 ∣ 𝜒}) = {𝑦 ∣ (𝑦 ∈ {𝑥 ∣ 𝜓} ∧ 𝑦 ∈ {𝑥 ∣ 𝜒})}
2		df-clab 2717	. . . . . . 7 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜓} ↔ [𝑦 / 𝑥]𝜓)
3	2	bicomi 223	. . . . . 6 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝑦 ∈ {𝑥 ∣ 𝜓})
4		df-clab 2717	. . . . . . 7 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜒} ↔ [𝑦 / 𝑥]𝜒)
5	4	bicomi 223	. . . . . 6 ⊢ ([𝑦 / 𝑥]𝜒 ↔ 𝑦 ∈ {𝑥 ∣ 𝜒})
6	3, 5	anbi12i 626	. . . . 5 ⊢ (([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ (𝑦 ∈ {𝑥 ∣ 𝜓} ∧ 𝑦 ∈ {𝑥 ∣ 𝜒}))
7	6	abbii 2809	. . . 4 ⊢ {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} = {𝑦 ∣ (𝑦 ∈ {𝑥 ∣ 𝜓} ∧ 𝑦 ∈ {𝑥 ∣ 𝜒})}
8		sbequ 2089	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜓 ↔ [𝑧 / 𝑥]𝜓))
9		sbequ 2089	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜒 ↔ [𝑧 / 𝑥]𝜒))
10	8, 9	anbi12d 630	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ ([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒)))
11	10	sbievw 2098	. . . . . . 7 ⊢ ([𝑧 / 𝑦]([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ ([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒))
12		ax-1 6	. . . . . . . . . 10 ⊢ ([𝑧 / 𝑥]𝜓 → ([𝑧 / 𝑥]𝜒 → [𝑧 / 𝑥]𝜓))
13	12	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 → ([𝑧 / 𝑥]𝜒 → [𝑧 / 𝑥]𝜓)))
14	13	impd 410	. . . . . . . 8 ⊢ (𝜑 → (([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒) → [𝑧 / 𝑥]𝜓))
15		ss2abdv.1	. . . . . . . . . 10 ⊢ (𝜑 → (𝜓 → 𝜒))
16	15	sbimdv 2084	. . . . . . . . 9 ⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜒))
17	16	ancld 550	. . . . . . . 8 ⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 → ([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒)))
18	14, 17	impbid 211	. . . . . . 7 ⊢ (𝜑 → (([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒) ↔ [𝑧 / 𝑥]𝜓))
19	11, 18	syl5bb 282	. . . . . 6 ⊢ (𝜑 → ([𝑧 / 𝑦]([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ [𝑧 / 𝑥]𝜓))
20		df-clab 2717	. . . . . 6 ⊢ (𝑧 ∈ {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} ↔ [𝑧 / 𝑦]([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒))
21		df-clab 2717	. . . . . 6 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜓} ↔ [𝑧 / 𝑥]𝜓)
22	19, 20, 21	3bitr4g 313	. . . . 5 ⊢ (𝜑 → (𝑧 ∈ {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} ↔ 𝑧 ∈ {𝑥 ∣ 𝜓}))
23	22	eqrdv 2737	. . . 4 ⊢ (𝜑 → {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} = {𝑥 ∣ 𝜓})
24	7, 23	eqtr3id 2793	. . 3 ⊢ (𝜑 → {𝑦 ∣ (𝑦 ∈ {𝑥 ∣ 𝜓} ∧ 𝑦 ∈ {𝑥 ∣ 𝜒})} = {𝑥 ∣ 𝜓})
25	1, 24	eqtrid 2791	. 2 ⊢ (𝜑 → ({𝑥 ∣ 𝜓} ∩ {𝑥 ∣ 𝜒}) = {𝑥 ∣ 𝜓})
26		df-ss 3908	. 2 ⊢ ({𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝜒} ↔ ({𝑥 ∣ 𝜓} ∩ {𝑥 ∣ 𝜒}) = {𝑥 ∣ 𝜓})
27	25, 26	sylibr 233	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝜒})

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  [wsb 2070   ∈ wcel 2109  {cab 2716   ∩ cin 3890   ⊆ wss 3891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-in 3898  df-ss 3908

This theorem is referenced by:  ss2abi  4004  intss  4905  ssopab2  5460  ssoprab2  7334  suppimacnvss  7973  suppimacnv  7974  ressuppss  7983  ss2ixp  8672  fiss  9144  tcss  9485  tcel  9486  infmap2  9958  cfub  9989  cflm  9990  cflecard  9993  clsslem  14676  cncmet  24467  plyss  25341  iunrnmptss  30884  ofrn2  30956  sigaclci  32079  subfacp1lem6  33126  ss2mcls  33509  itg2addnclem  35807  sdclem1  35880  istotbnd3  35908  sstotbnd  35912  qsss1  36402  sticksstones4  40085  sticksstones14  40096  sticksstones20  40102  sticksstones22  40104  aomclem4  40862  hbtlem4  40931  hbtlem3  40932  rngunsnply  40978  iocinico  41023