Theorem intab 3860

Description: The intersection of a special case of a class abstraction. 𝑦 may be free in 𝜑 and 𝐴, which can be thought of a 𝜑(𝑦) and 𝐴(𝑦). (Contributed by NM, 28-Jul-2006.) (Proof shortened by Mario Carneiro, 14-Nov-2016.)

Hypotheses

Ref	Expression
intab.1	⊢ 𝐴 ∈ V
intab.2	⊢ {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)} ∈ V

Assertion

Ref	Expression
intab	⊢ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} = {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)}

Distinct variable groups:   𝑥,𝐴   𝜑,𝑥   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑦)   𝐴(𝑦)

Proof of Theorem intab

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq1 2177	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → (𝑧 = 𝐴 ↔ 𝑥 = 𝐴))
2	1	anbi2d 461	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → ((𝜑 ∧ 𝑧 = 𝐴) ↔ (𝜑 ∧ 𝑥 = 𝐴)))
3	2	exbidv 1818	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (∃𝑦(𝜑 ∧ 𝑧 = 𝐴) ↔ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)))
4	3	cbvabv 2295	. . . . . . 7 ⊢ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} = {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)}
5		intab.2	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)} ∈ V
6	4, 5	eqeltri 2243	. . . . . 6 ⊢ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} ∈ V
7		nfe1 1489	. . . . . . . . 9 ⊢ Ⅎ𝑦∃𝑦(𝜑 ∧ 𝑧 = 𝐴)
8	7	nfab 2317	. . . . . . . 8 ⊢ Ⅎ𝑦{𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}
9	8	nfeq2 2324	. . . . . . 7 ⊢ Ⅎ𝑦 𝑥 = {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}
10		eleq2 2234	. . . . . . . 8 ⊢ (𝑥 = {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}))
11	10	imbi2d 229	. . . . . . 7 ⊢ (𝑥 = {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} → ((𝜑 → 𝐴 ∈ 𝑥) ↔ (𝜑 → 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)})))
12	9, 11	albid 1608	. . . . . 6 ⊢ (𝑥 = {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} → (∀𝑦(𝜑 → 𝐴 ∈ 𝑥) ↔ ∀𝑦(𝜑 → 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)})))
13	6, 12	elab 2874	. . . . 5 ⊢ ({𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} ∈ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} ↔ ∀𝑦(𝜑 → 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}))
14		19.8a 1583	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 = 𝐴) → ∃𝑦(𝜑 ∧ 𝑧 = 𝐴))
15	14	ex 114	. . . . . . . 8 ⊢ (𝜑 → (𝑧 = 𝐴 → ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)))
16	15	alrimiv 1867	. . . . . . 7 ⊢ (𝜑 → ∀𝑧(𝑧 = 𝐴 → ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)))
17		intab.1	. . . . . . . 8 ⊢ 𝐴 ∈ V
18	17	sbc6 2980	. . . . . . 7 ⊢ ([𝐴 / 𝑧]∃𝑦(𝜑 ∧ 𝑧 = 𝐴) ↔ ∀𝑧(𝑧 = 𝐴 → ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)))
19	16, 18	sylibr 133	. . . . . 6 ⊢ (𝜑 → [𝐴 / 𝑧]∃𝑦(𝜑 ∧ 𝑧 = 𝐴))
20		df-sbc 2956	. . . . . 6 ⊢ ([𝐴 / 𝑧]∃𝑦(𝜑 ∧ 𝑧 = 𝐴) ↔ 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)})
21	19, 20	sylib 121	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)})
22	13, 21	mpgbir 1446	. . . 4 ⊢ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} ∈ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)}
23		intss1 3846	. . . 4 ⊢ ({𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} ∈ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} → ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} ⊆ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)})
24	22, 23	ax-mp 5	. . 3 ⊢ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} ⊆ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}
25		19.29r 1614	. . . . . . . 8 ⊢ ((∃𝑦(𝜑 ∧ 𝑧 = 𝐴) ∧ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)) → ∃𝑦((𝜑 ∧ 𝑧 = 𝐴) ∧ (𝜑 → 𝐴 ∈ 𝑥)))
26		simplr 525	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ (𝜑 → 𝐴 ∈ 𝑥)) → 𝑧 = 𝐴)
27		pm3.35 345	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝜑 → 𝐴 ∈ 𝑥)) → 𝐴 ∈ 𝑥)
28	27	adantlr 474	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ (𝜑 → 𝐴 ∈ 𝑥)) → 𝐴 ∈ 𝑥)
29	26, 28	eqeltrd 2247	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ (𝜑 → 𝐴 ∈ 𝑥)) → 𝑧 ∈ 𝑥)
30	29	exlimiv 1591	. . . . . . . 8 ⊢ (∃𝑦((𝜑 ∧ 𝑧 = 𝐴) ∧ (𝜑 → 𝐴 ∈ 𝑥)) → 𝑧 ∈ 𝑥)
31	25, 30	syl 14	. . . . . . 7 ⊢ ((∃𝑦(𝜑 ∧ 𝑧 = 𝐴) ∧ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)) → 𝑧 ∈ 𝑥)
32	31	ex 114	. . . . . 6 ⊢ (∃𝑦(𝜑 ∧ 𝑧 = 𝐴) → (∀𝑦(𝜑 → 𝐴 ∈ 𝑥) → 𝑧 ∈ 𝑥))
33	32	alrimiv 1867	. . . . 5 ⊢ (∃𝑦(𝜑 ∧ 𝑧 = 𝐴) → ∀𝑥(∀𝑦(𝜑 → 𝐴 ∈ 𝑥) → 𝑧 ∈ 𝑥))
34		vex 2733	. . . . . 6 ⊢ 𝑧 ∈ V
35	34	elintab 3842	. . . . 5 ⊢ (𝑧 ∈ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} ↔ ∀𝑥(∀𝑦(𝜑 → 𝐴 ∈ 𝑥) → 𝑧 ∈ 𝑥))
36	33, 35	sylibr 133	. . . 4 ⊢ (∃𝑦(𝜑 ∧ 𝑧 = 𝐴) → 𝑧 ∈ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)})
37	36	abssi 3222	. . 3 ⊢ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} ⊆ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)}
38	24, 37	eqssi 3163	. 2 ⊢ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} = {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}
39	38, 4	eqtri 2191	1 ⊢ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} = {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)}

Syntax hints:   → wi 4   ∧ wa 103  ∀wal 1346   = wceq 1348  ∃wex 1485   ∈ wcel 2141  {cab 2156  Vcvv 2730  [wsbc 2955   ⊆ wss 3121  ∩ cint 3831

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-sbc 2956  df-in 3127  df-ss 3134  df-int 3832

This theorem is referenced by: (None)