Theorem axsepg3 35329

Description: A generalization of ax-sep 5225 in which 𝑦 and 𝑧 need not be distinct. This theorem scheme bundles ax-sep 5225 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 2380. (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 1921	. . 3 ⊢ Ⅎ𝑥 ¬ ∀𝑦 𝑦 = 𝑧
2		nfvd 1922	. . . 4 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦 𝑥 ∈ 𝑤)
3		nfcvf 2928	. . . . . 6 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦𝑧)
4	3	nfcrd 2896	. . . . 5 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦 𝑥 ∈ 𝑧)
5		nfvd 1922	. . . . 5 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦𝜑)
6	4, 5	nfand 1904	. . . 4 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦(𝑥 ∈ 𝑧 ∧ 𝜑))
7	2, 6	nfbid 1909	. . 3 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦(𝑥 ∈ 𝑤 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
8	1, 7	nfald 2337	. 2 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦∀𝑥(𝑥 ∈ 𝑤 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
9		nfvd 1922	. 2 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑤∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
10		elequ2 2134	. . . . . 6 ⊢ (𝑤 = 𝑦 → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦))
11	10	bibi1d 344	. . . . 5 ⊢ (𝑤 = 𝑦 → ((𝑥 ∈ 𝑤 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) ↔ (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))))
12	11	biimpd 230	. . . 4 ⊢ (𝑤 = 𝑦 → ((𝑥 ∈ 𝑤 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) → (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))))
13	12	alimdv 1923	. . 3 ⊢ (𝑤 = 𝑦 → (∀𝑥(𝑥 ∈ 𝑤 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) → ∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))))
14	13	a1i 11	. 2 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (𝑤 = 𝑦 → (∀𝑥(𝑥 ∈ 𝑤 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) → ∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))))
15		elequ2 2134	. . . . . . 7 ⊢ (𝑦 = 𝑧 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧))
16	15	anbi1d 637	. . . . . 6 ⊢ (𝑦 = 𝑧 → ((𝑥 ∈ 𝑦 ∧ 𝜑) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
17	16	bibi2d 343	. . . . 5 ⊢ (𝑦 = 𝑧 → ((𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑦 ∧ 𝜑)) ↔ (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))))
18	17	biimpd 230	. . . 4 ⊢ (𝑦 = 𝑧 → ((𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑦 ∧ 𝜑)) → (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))))
19	18	alimdv 1923	. . 3 ⊢ (𝑦 = 𝑧 → (∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑦 ∧ 𝜑)) → ∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))))
20	19	sps 2197	. 2 ⊢ (∀𝑦 𝑦 = 𝑧 → (∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑦 ∧ 𝜑)) → ∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))))
21		ax-sep 5225	. 2 ⊢ ∃𝑤∀𝑥(𝑥 ∈ 𝑤 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
22		ax-nul 5235	. . 3 ⊢ ∃𝑦∀𝑥 ¬ 𝑥 ∈ 𝑦
23		id 22	. . . . 5 ⊢ (¬ 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑦)
24	23	bianfd 539	. . . 4 ⊢ (¬ 𝑥 ∈ 𝑦 → (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑦 ∧ 𝜑)))
25	24	alimi 1818	. . 3 ⊢ (∀𝑥 ¬ 𝑥 ∈ 𝑦 → ∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑦 ∧ 𝜑)))
26	22, 25	eximii 1844	. 2 ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑦 ∧ 𝜑))
27	8, 9, 14, 20, 21, 26	dvelimexcasei 35267	1 ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396  ∀wal 1545  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-13 2380  ax-sep 5225  ax-nul 5235

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791  df-clel 2815  df-nfc 2889

This theorem is referenced by:  axsepg5  35332