Theorem intab 4937

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 7964 or abexssex 7965 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 2764	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → (𝑧 = 𝐴 ↔ 𝑥 = 𝐴))
2	1	anbi2d 642	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → ((𝜑 ∧ 𝑧 = 𝐴) ↔ (𝜑 ∧ 𝑥 = 𝐴)))
3	2	exbidv 1954	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (∃𝑦(𝜑 ∧ 𝑧 = 𝐴) ↔ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)))
4	3	cbvabv 2830	. . . . . . 7 ⊢ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} = {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)}
5		intab.2	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)} ∈ V
6	4, 5	eqeltri 2856	. . . . . 6 ⊢ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} ∈ V
7		nfe1 2187	. . . . . . . . 9 ⊢ Ⅎ𝑦∃𝑦(𝜑 ∧ 𝑧 = 𝐴)
8	7	nfab 2928	. . . . . . . 8 ⊢ Ⅎ𝑦{𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}
9	8	nfeq2 2939	. . . . . . 7 ⊢ Ⅎ𝑦 𝑥 = {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}
10		eleq2 2849	. . . . . . . 8 ⊢ (𝑥 = {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}))
11	10	imbi2d 343	. . . . . . 7 ⊢ (𝑥 = {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} → ((𝜑 → 𝐴 ∈ 𝑥) ↔ (𝜑 → 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)})))
12	9, 11	albid 2258	. . . . . 6 ⊢ (𝑥 = {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} → (∀𝑦(𝜑 → 𝐴 ∈ 𝑥) ↔ ∀𝑦(𝜑 → 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)})))
13	6, 12	elab 3632	. . . . 5 ⊢ ({𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} ∈ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} ↔ ∀𝑦(𝜑 → 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}))
14		19.8a 2217	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 = 𝐴) → ∃𝑦(𝜑 ∧ 𝑧 = 𝐴))
15	14	ex 418	. . . . . . . 8 ⊢ (𝜑 → (𝑧 = 𝐴 → ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)))
16	15	alrimiv 1960	. . . . . . 7 ⊢ (𝜑 → ∀𝑧(𝑧 = 𝐴 → ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)))
17		intab.1	. . . . . . . 8 ⊢ 𝐴 ∈ V
18	17	sbc6 3769	. . . . . . 7 ⊢ ([𝐴 / 𝑧]∃𝑦(𝜑 ∧ 𝑧 = 𝐴) ↔ ∀𝑧(𝑧 = 𝐴 → ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)))
19	16, 18	sylibr 237	. . . . . 6 ⊢ (𝜑 → [𝐴 / 𝑧]∃𝑦(𝜑 ∧ 𝑧 = 𝐴))
20		df-sbc 3739	. . . . . 6 ⊢ ([𝐴 / 𝑧]∃𝑦(𝜑 ∧ 𝑧 = 𝐴) ↔ 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)})
21	19, 20	sylib 221	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)})
22	13, 21	mpgbir 1832	. . . 4 ⊢ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} ∈ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)}
23		intss1 4922	. . . 4 ⊢ ({𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} ∈ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} → ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} ⊆ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)})
24	22, 23	ax-mp 5	. . 3 ⊢ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} ⊆ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}
25		19.29r 1907	. . . . . . . 8 ⊢ ((∃𝑦(𝜑 ∧ 𝑧 = 𝐴) ∧ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)) → ∃𝑦((𝜑 ∧ 𝑧 = 𝐴) ∧ (𝜑 → 𝐴 ∈ 𝑥)))
26		simplr 781	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ (𝜑 → 𝐴 ∈ 𝑥)) → 𝑧 = 𝐴)
27		pm3.35 815	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝜑 → 𝐴 ∈ 𝑥)) → 𝐴 ∈ 𝑥)
28	27	adantlr 728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ (𝜑 → 𝐴 ∈ 𝑥)) → 𝐴 ∈ 𝑥)
29	26, 28	eqeltrd 2860	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 = 𝐴) ∧ (𝜑 → 𝐴 ∈ 𝑥)) → 𝑧 ∈ 𝑥)
30	29	exlimiv 1963	. . . . . . . 8 ⊢ (∃𝑦((𝜑 ∧ 𝑧 = 𝐴) ∧ (𝜑 → 𝐴 ∈ 𝑥)) → 𝑧 ∈ 𝑥)
31	25, 30	syl 18	. . . . . . 7 ⊢ ((∃𝑦(𝜑 ∧ 𝑧 = 𝐴) ∧ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)) → 𝑧 ∈ 𝑥)
32	31	ex 418	. . . . . 6 ⊢ (∃𝑦(𝜑 ∧ 𝑧 = 𝐴) → (∀𝑦(𝜑 → 𝐴 ∈ 𝑥) → 𝑧 ∈ 𝑥))
33	32	alrimiv 1960	. . . . 5 ⊢ (∃𝑦(𝜑 ∧ 𝑧 = 𝐴) → ∀𝑥(∀𝑦(𝜑 → 𝐴 ∈ 𝑥) → 𝑧 ∈ 𝑥))
34		vex 3454	. . . . . 6 ⊢ 𝑧 ∈ V
35	34	elintab 4918	. . . . 5 ⊢ (𝑧 ∈ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} ↔ ∀𝑥(∀𝑦(𝜑 → 𝐴 ∈ 𝑥) → 𝑧 ∈ 𝑥))
36	33, 35	sylibr 237	. . . 4 ⊢ (∃𝑦(𝜑 ∧ 𝑧 = 𝐴) → 𝑧 ∈ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)})
37	36	abssi 4015	. . 3 ⊢ {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)} ⊆ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)}
38	24, 37	eqssi 3946	. 2 ⊢ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} = {𝑧 ∣ ∃𝑦(𝜑 ∧ 𝑧 = 𝐴)}
39	38, 4	eqtri 2783	1 ⊢ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} = {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)}

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145  {cab 2738  Vcvv 3450  [wsbc 3738   ⊆ wss 3898  ∩ cint 4906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-v 3452  df-sbc 3739  df-ss 3915  df-int 4907

This theorem is used by: (None)