Theorem intab 4507

Description: The intersection of a special case of a class abstraction. 𝑦 may be free in 𝜑 and 𝐴, which can be thought of a 𝜑(𝑦) and 𝐴(𝑦). Typically, abrexex2 7148 or abexssex 7149 can be used to satisfy the second hypothesis. (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 2626	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → (𝑧 = 𝐴 ↔ 𝑥 = 𝐴))
2	1	anbi2d 740	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → ((𝜑 ∧ 𝑧 = 𝐴) ↔ (𝜑 ∧ 𝑥 = 𝐴)))
3	2	exbidv 1850	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (∃𝑦(𝜑 ∧ 𝑧 = 𝐴) ↔ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)))
4	3	cbvabv 2747	. . . . . . 7 ⊢ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} = {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)}
5		intab.2	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)} ∈ V
6	4, 5	eqeltri 2697	. . . . . 6 ⊢ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} ∈ V
7		nfe1 2027	. . . . . . . . 9 ⊢ Ⅎ𝑦∃𝑦(𝜑 ∧ 𝑧 = 𝐴)
8	7	nfab 2769	. . . . . . . 8 ⊢ Ⅎ𝑦{𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}
9	8	nfeq2 2780	. . . . . . 7 ⊢ Ⅎ𝑦 𝑥 = {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}
10		eleq2 2690	. . . . . . . 8 ⊢ (𝑥 = {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}))
11	10	imbi2d 330	. . . . . . 7 ⊢ (𝑥 = {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} → ((𝜑 → 𝐴 ∈ 𝑥) ↔ (𝜑 → 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)})))
12	9, 11	albid 2090	. . . . . 6 ⊢ (𝑥 = {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} → (∀𝑦(𝜑 → 𝐴 ∈ 𝑥) ↔ ∀𝑦(𝜑 → 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)})))
13	6, 12	elab 3350	. . . . 5 ⊢ ({𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} ∈ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} ↔ ∀𝑦(𝜑 → 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}))
14		19.8a 2052	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 = 𝐴) → ∃𝑦(𝜑 ∧ 𝑧 = 𝐴))
15	14	ex 450	. . . . . . . 8 ⊢ (𝜑 → (𝑧 = 𝐴 → ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)))
16	15	alrimiv 1855	. . . . . . 7 ⊢ (𝜑 → ∀𝑧(𝑧 = 𝐴 → ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)))
17		intab.1	. . . . . . . 8 ⊢ 𝐴 ∈ V
18	17	sbc6 3462	. . . . . . 7 ⊢ ([𝐴 / 𝑧]∃𝑦(𝜑 ∧ 𝑧 = 𝐴) ↔ ∀𝑧(𝑧 = 𝐴 → ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)))
19	16, 18	sylibr 224	. . . . . 6 ⊢ (𝜑 → [𝐴 / 𝑧]∃𝑦(𝜑 ∧ 𝑧 = 𝐴))
20		df-sbc 3436	. . . . . 6 ⊢ ([𝐴 / 𝑧]∃𝑦(𝜑 ∧ 𝑧 = 𝐴) ↔ 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)})
21	19, 20	sylib 208	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)})
22	13, 21	mpgbir 1726	. . . 4 ⊢ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} ∈ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)}
23		intss1 4492	. . . 4 ⊢ ({𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} ∈ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} → ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} ⊆ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)})
24	22, 23	ax-mp 5	. . 3 ⊢ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} ⊆ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}
25		19.29r 1802	. . . . . . . 8 ⊢ ((∃𝑦(𝜑 ∧ 𝑧 = 𝐴) ∧ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)) → ∃𝑦((𝜑 ∧ 𝑧 = 𝐴) ∧ (𝜑 → 𝐴 ∈ 𝑥)))
26		simplr 792	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ (𝜑 → 𝐴 ∈ 𝑥)) → 𝑧 = 𝐴)
27		pm3.35 611	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝜑 → 𝐴 ∈ 𝑥)) → 𝐴 ∈ 𝑥)
28	27	adantlr 751	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ (𝜑 → 𝐴 ∈ 𝑥)) → 𝐴 ∈ 𝑥)
29	26, 28	eqeltrd 2701	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ (𝜑 → 𝐴 ∈ 𝑥)) → 𝑧 ∈ 𝑥)
30	29	exlimiv 1858	. . . . . . . 8 ⊢ (∃𝑦((𝜑 ∧ 𝑧 = 𝐴) ∧ (𝜑 → 𝐴 ∈ 𝑥)) → 𝑧 ∈ 𝑥)
31	25, 30	syl 17	. . . . . . 7 ⊢ ((∃𝑦(𝜑 ∧ 𝑧 = 𝐴) ∧ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)) → 𝑧 ∈ 𝑥)
32	31	ex 450	. . . . . 6 ⊢ (∃𝑦(𝜑 ∧ 𝑧 = 𝐴) → (∀𝑦(𝜑 → 𝐴 ∈ 𝑥) → 𝑧 ∈ 𝑥))
33	32	alrimiv 1855	. . . . 5 ⊢ (∃𝑦(𝜑 ∧ 𝑧 = 𝐴) → ∀𝑥(∀𝑦(𝜑 → 𝐴 ∈ 𝑥) → 𝑧 ∈ 𝑥))
34		vex 3203	. . . . . 6 ⊢ 𝑧 ∈ V
35	34	elintab 4487	. . . . 5 ⊢ (𝑧 ∈ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} ↔ ∀𝑥(∀𝑦(𝜑 → 𝐴 ∈ 𝑥) → 𝑧 ∈ 𝑥))
36	33, 35	sylibr 224	. . . 4 ⊢ (∃𝑦(𝜑 ∧ 𝑧 = 𝐴) → 𝑧 ∈ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)})
37	36	abssi 3677	. . 3 ⊢ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} ⊆ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)}
38	24, 37	eqssi 3619	. 2 ⊢ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} = {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}
39	38, 4	eqtri 2644	1 ⊢ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} = {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)}

Syntax hints:   → wi 4   ∧ wa 384  ∀wal 1481   = wceq 1483  ∃wex 1704   ∈ wcel 1990  {cab 2608  Vcvv 3200  [wsbc 3435   ⊆ wss 3574  ∩ cint 4475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-sbc 3436  df-in 3581  df-ss 3588  df-int 4476

This theorem is referenced by: (None)