Theorem intab 3899

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 2200	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → (𝑧 = 𝐴 ↔ 𝑥 = 𝐴))
2	1	anbi2d 464	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → ((𝜑 ∧ 𝑧 = 𝐴) ↔ (𝜑 ∧ 𝑥 = 𝐴)))
3	2	exbidv 1836	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (∃𝑦(𝜑 ∧ 𝑧 = 𝐴) ↔ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)))
4	3	cbvabv 2318	. . . . . . 7 ⊢ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} = {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)}
5		intab.2	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)} ∈ V
6	4, 5	eqeltri 2266	. . . . . 6 ⊢ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} ∈ V
7		nfe1 1507	. . . . . . . . 9 ⊢ Ⅎ𝑦∃𝑦(𝜑 ∧ 𝑧 = 𝐴)
8	7	nfab 2341	. . . . . . . 8 ⊢ Ⅎ𝑦{𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}
9	8	nfeq2 2348	. . . . . . 7 ⊢ Ⅎ𝑦 𝑥 = {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}
10		eleq2 2257	. . . . . . . 8 ⊢ (𝑥 = {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}))
11	10	imbi2d 230	. . . . . . 7 ⊢ (𝑥 = {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} → ((𝜑 → 𝐴 ∈ 𝑥) ↔ (𝜑 → 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)})))
12	9, 11	albid 1626	. . . . . 6 ⊢ (𝑥 = {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} → (∀𝑦(𝜑 → 𝐴 ∈ 𝑥) ↔ ∀𝑦(𝜑 → 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)})))
13	6, 12	elab 2904	. . . . 5 ⊢ ({𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} ∈ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} ↔ ∀𝑦(𝜑 → 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}))
14		19.8a 1601	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 = 𝐴) → ∃𝑦(𝜑 ∧ 𝑧 = 𝐴))
15	14	ex 115	. . . . . . . 8 ⊢ (𝜑 → (𝑧 = 𝐴 → ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)))
16	15	alrimiv 1885	. . . . . . 7 ⊢ (𝜑 → ∀𝑧(𝑧 = 𝐴 → ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)))
17		intab.1	. . . . . . . 8 ⊢ 𝐴 ∈ V
18	17	sbc6 3011	. . . . . . 7 ⊢ ([𝐴 / 𝑧]∃𝑦(𝜑 ∧ 𝑧 = 𝐴) ↔ ∀𝑧(𝑧 = 𝐴 → ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)))
19	16, 18	sylibr 134	. . . . . 6 ⊢ (𝜑 → [𝐴 / 𝑧]∃𝑦(𝜑 ∧ 𝑧 = 𝐴))
20		df-sbc 2986	. . . . . 6 ⊢ ([𝐴 / 𝑧]∃𝑦(𝜑 ∧ 𝑧 = 𝐴) ↔ 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)})
21	19, 20	sylib 122	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)})
22	13, 21	mpgbir 1464	. . . 4 ⊢ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} ∈ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)}
23		intss1 3885	. . . 4 ⊢ ({𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} ∈ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} → ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} ⊆ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)})
24	22, 23	ax-mp 5	. . 3 ⊢ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} ⊆ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}
25		19.29r 1632	. . . . . . . 8 ⊢ ((∃𝑦(𝜑 ∧ 𝑧 = 𝐴) ∧ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)) → ∃𝑦((𝜑 ∧ 𝑧 = 𝐴) ∧ (𝜑 → 𝐴 ∈ 𝑥)))
26		simplr 528	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ (𝜑 → 𝐴 ∈ 𝑥)) → 𝑧 = 𝐴)
27		pm3.35 347	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝜑 → 𝐴 ∈ 𝑥)) → 𝐴 ∈ 𝑥)
28	27	adantlr 477	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ (𝜑 → 𝐴 ∈ 𝑥)) → 𝐴 ∈ 𝑥)
29	26, 28	eqeltrd 2270	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ (𝜑 → 𝐴 ∈ 𝑥)) → 𝑧 ∈ 𝑥)
30	29	exlimiv 1609	. . . . . . . 8 ⊢ (∃𝑦((𝜑 ∧ 𝑧 = 𝐴) ∧ (𝜑 → 𝐴 ∈ 𝑥)) → 𝑧 ∈ 𝑥)
31	25, 30	syl 14	. . . . . . 7 ⊢ ((∃𝑦(𝜑 ∧ 𝑧 = 𝐴) ∧ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)) → 𝑧 ∈ 𝑥)
32	31	ex 115	. . . . . 6 ⊢ (∃𝑦(𝜑 ∧ 𝑧 = 𝐴) → (∀𝑦(𝜑 → 𝐴 ∈ 𝑥) → 𝑧 ∈ 𝑥))
33	32	alrimiv 1885	. . . . 5 ⊢ (∃𝑦(𝜑 ∧ 𝑧 = 𝐴) → ∀𝑥(∀𝑦(𝜑 → 𝐴 ∈ 𝑥) → 𝑧 ∈ 𝑥))
34		vex 2763	. . . . . 6 ⊢ 𝑧 ∈ V
35	34	elintab 3881	. . . . 5 ⊢ (𝑧 ∈ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} ↔ ∀𝑥(∀𝑦(𝜑 → 𝐴 ∈ 𝑥) → 𝑧 ∈ 𝑥))
36	33, 35	sylibr 134	. . . 4 ⊢ (∃𝑦(𝜑 ∧ 𝑧 = 𝐴) → 𝑧 ∈ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)})
37	36	abssi 3254	. . 3 ⊢ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} ⊆ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)}
38	24, 37	eqssi 3195	. 2 ⊢ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} = {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}
39	38, 4	eqtri 2214	1 ⊢ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} = {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)}

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1362   = wceq 1364  ∃wex 1503   ∈ wcel 2164  {cab 2179  Vcvv 2760  [wsbc 2985   ⊆ wss 3153  ∩ cint 3870

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-sbc 2986  df-in 3159  df-ss 3166  df-int 3871

This theorem is referenced by: (None)