Theorem axsepg3 35449

Description: A generalization of ax-sep 5251 in which 𝑦 and 𝑧 need not be distinct. This theorem scheme bundles ax-sep 5251 with the degenerate instance ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑦 ∧ 𝜑)) which is satisfied by the existence of the empty set. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by BTernaryTau, 3-Aug-2025.) (New usage is discouraged.)

Assertion

Ref	Expression
axsepg3	⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))

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

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem axsepg3

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1937	. . 3 ⊢ Ⅎ𝑥 ¬ ∀𝑦 𝑦 = 𝑧
2		nfvd 1938	. . . 4 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦 𝑥 ∈ 𝑤)
3		nfcvf 2953	. . . . . 6 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦𝑧)
4	3	nfcrd 2921	. . . . 5 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦 𝑥 ∈ 𝑧)
5		nfvd 1938	. . . . 5 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦𝜑)
6	4, 5	nfand 1920	. . . 4 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦(𝑥 ∈ 𝑧 ∧ 𝜑))
7	2, 6	nfbid 1925	. . 3 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦(𝑥 ∈ 𝑤 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
8	1, 7	nfald 2363	. 2 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦∀𝑥(𝑥 ∈ 𝑤 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
9		nfvd 1938	. 2 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑤∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
10		elequ2 2160	. . . . . 6 ⊢ (𝑤 = 𝑦 → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦))
11	10	bibi1d 346	. . . . 5 ⊢ (𝑤 = 𝑦 → ((𝑥 ∈ 𝑤 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) ↔ (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))))
12	11	biimpd 232	. . . 4 ⊢ (𝑤 = 𝑦 → ((𝑥 ∈ 𝑤 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) → (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))))
13	12	alimdv 1939	. . 3 ⊢ (𝑤 = 𝑦 → (∀𝑥(𝑥 ∈ 𝑤 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) → ∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))))
14	13	a1i 11	. 2 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (𝑤 = 𝑦 → (∀𝑥(𝑥 ∈ 𝑤 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) → ∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))))
15		elequ2 2160	. . . . . . 7 ⊢ (𝑦 = 𝑧 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧))
16	15	anbi1d 642	. . . . . 6 ⊢ (𝑦 = 𝑧 → ((𝑥 ∈ 𝑦 ∧ 𝜑) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
17	16	bibi2d 345	. . . . 5 ⊢ (𝑦 = 𝑧 → ((𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑦 ∧ 𝜑)) ↔ (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))))
18	17	biimpd 232	. . . 4 ⊢ (𝑦 = 𝑧 → ((𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑦 ∧ 𝜑)) → (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))))
19	18	alimdv 1939	. . 3 ⊢ (𝑦 = 𝑧 → (∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑦 ∧ 𝜑)) → ∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))))
20	19	sps 2223	. 2 ⊢ (∀𝑦 𝑦 = 𝑧 → (∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑦 ∧ 𝜑)) → ∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))))
21		ax-sep 5251	. 2 ⊢ ∃𝑤∀𝑥(𝑥 ∈ 𝑤 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
22		ax-nul 5261	. . 3 ⊢ ∃𝑦∀𝑥 ¬ 𝑥 ∈ 𝑦
23		id 23	. . . . 5 ⊢ (¬ 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑦)
24	23	bianfd 543	. . . 4 ⊢ (¬ 𝑥 ∈ 𝑦 → (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑦 ∧ 𝜑)))
25	24	alimi 1834	. . 3 ⊢ (∀𝑥 ¬ 𝑥 ∈ 𝑦 → ∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑦 ∧ 𝜑)))
26	22, 25	eximii 1860	. 2 ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑦 ∧ 𝜑))
27	8, 9, 14, 20, 21, 26	dvelimexcasei 35383	1 ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1561  ∃wex 1802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-13 2406  ax-sep 5251  ax-nul 5261

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-nf 1807  df-clel 2840  df-nfc 2914

This theorem is referenced by:  axsepg5  35452