Theorem intab 4872

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 7681 or abexssex 7682 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 2763	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → (𝑧 = 𝐴 ↔ 𝑥 = 𝐴))
2	1	anbi2d 631	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → ((𝜑 ∧ 𝑧 = 𝐴) ↔ (𝜑 ∧ 𝑥 = 𝐴)))
3	2	exbidv 1923	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (∃𝑦(𝜑 ∧ 𝑧 = 𝐴) ↔ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)))
4	3	cbvabv 2827	. . . . . . 7 ⊢ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} = {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)}
5		intab.2	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)} ∈ V
6	4, 5	eqeltri 2849	. . . . . 6 ⊢ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} ∈ V
7		nfe1 2152	. . . . . . . . 9 ⊢ Ⅎ𝑦∃𝑦(𝜑 ∧ 𝑧 = 𝐴)
8	7	nfab 2926	. . . . . . . 8 ⊢ Ⅎ𝑦{𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}
9	8	nfeq2 2937	. . . . . . 7 ⊢ Ⅎ𝑦 𝑥 = {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}
10		eleq2 2841	. . . . . . . 8 ⊢ (𝑥 = {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}))
11	10	imbi2d 344	. . . . . . 7 ⊢ (𝑥 = {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} → ((𝜑 → 𝐴 ∈ 𝑥) ↔ (𝜑 → 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)})))
12	9, 11	albid 2223	. . . . . 6 ⊢ (𝑥 = {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} → (∀𝑦(𝜑 → 𝐴 ∈ 𝑥) ↔ ∀𝑦(𝜑 → 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)})))
13	6, 12	elab 3591	. . . . 5 ⊢ ({𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} ∈ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} ↔ ∀𝑦(𝜑 → 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}))
14		19.8a 2179	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 = 𝐴) → ∃𝑦(𝜑 ∧ 𝑧 = 𝐴))
15	14	ex 416	. . . . . . . 8 ⊢ (𝜑 → (𝑧 = 𝐴 → ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)))
16	15	alrimiv 1929	. . . . . . 7 ⊢ (𝜑 → ∀𝑧(𝑧 = 𝐴 → ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)))
17		intab.1	. . . . . . . 8 ⊢ 𝐴 ∈ V
18	17	sbc6 3730	. . . . . . 7 ⊢ ([𝐴 / 𝑧]∃𝑦(𝜑 ∧ 𝑧 = 𝐴) ↔ ∀𝑧(𝑧 = 𝐴 → ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)))
19	16, 18	sylibr 237	. . . . . 6 ⊢ (𝜑 → [𝐴 / 𝑧]∃𝑦(𝜑 ∧ 𝑧 = 𝐴))
20		df-sbc 3700	. . . . . 6 ⊢ ([𝐴 / 𝑧]∃𝑦(𝜑 ∧ 𝑧 = 𝐴) ↔ 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)})
21	19, 20	sylib 221	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)})
22	13, 21	mpgbir 1802	. . . 4 ⊢ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} ∈ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)}
23		intss1 4857	. . . 4 ⊢ ({𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} ∈ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} → ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} ⊆ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)})
24	22, 23	ax-mp 5	. . 3 ⊢ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} ⊆ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}
25		19.29r 1876	. . . . . . . 8 ⊢ ((∃𝑦(𝜑 ∧ 𝑧 = 𝐴) ∧ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)) → ∃𝑦((𝜑 ∧ 𝑧 = 𝐴) ∧ (𝜑 → 𝐴 ∈ 𝑥)))
26		simplr 768	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ (𝜑 → 𝐴 ∈ 𝑥)) → 𝑧 = 𝐴)
27		pm3.35 802	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝜑 → 𝐴 ∈ 𝑥)) → 𝐴 ∈ 𝑥)
28	27	adantlr 714	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ (𝜑 → 𝐴 ∈ 𝑥)) → 𝐴 ∈ 𝑥)
29	26, 28	eqeltrd 2853	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ (𝜑 → 𝐴 ∈ 𝑥)) → 𝑧 ∈ 𝑥)
30	29	exlimiv 1932	. . . . . . . 8 ⊢ (∃𝑦((𝜑 ∧ 𝑧 = 𝐴) ∧ (𝜑 → 𝐴 ∈ 𝑥)) → 𝑧 ∈ 𝑥)
31	25, 30	syl 17	. . . . . . 7 ⊢ ((∃𝑦(𝜑 ∧ 𝑧 = 𝐴) ∧ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)) → 𝑧 ∈ 𝑥)
32	31	ex 416	. . . . . 6 ⊢ (∃𝑦(𝜑 ∧ 𝑧 = 𝐴) → (∀𝑦(𝜑 → 𝐴 ∈ 𝑥) → 𝑧 ∈ 𝑥))
33	32	alrimiv 1929	. . . . 5 ⊢ (∃𝑦(𝜑 ∧ 𝑧 = 𝐴) → ∀𝑥(∀𝑦(𝜑 → 𝐴 ∈ 𝑥) → 𝑧 ∈ 𝑥))
34		vex 3414	. . . . . 6 ⊢ 𝑧 ∈ V
35	34	elintab 4853	. . . . 5 ⊢ (𝑧 ∈ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} ↔ ∀𝑥(∀𝑦(𝜑 → 𝐴 ∈ 𝑥) → 𝑧 ∈ 𝑥))
36	33, 35	sylibr 237	. . . 4 ⊢ (∃𝑦(𝜑 ∧ 𝑧 = 𝐴) → 𝑧 ∈ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)})
37	36	abssi 3977	. . 3 ⊢ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} ⊆ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)}
38	24, 37	eqssi 3911	. 2 ⊢ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} = {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}
39	38, 4	eqtri 2782	1 ⊢ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} = {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)}

Syntax hints:   → wi 4   ∧ wa 399  ∀wal 1537   = wceq 1539  ∃wex 1782   ∈ wcel 2112  {cab 2736  Vcvv 3410  [wsbc 3699   ⊆ wss 3861  ∩ cint 4842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-v 3412  df-sbc 3700  df-in 3868  df-ss 3878  df-int 4843

This theorem is referenced by: (None)