Theorem srepdf 36006

Description: Derive the strong version of the Axiom Scheme of Replacement used in wfaxrep 46077 (see comments there) from a particular instance of that version of Replacement. Note that this theorem depends on ax-rep 5231, so it does not follow that we could replace ax-rep 5231 with an axiom that lacks a wff metavariable. (Contributed by BTernaryTau, 30-Sep-2026.)

Hypotheses

Ref	Expression
srepdf.1	⊢ Ⅎ𝑓𝜑
srepdf.2	⊢ Ⅎ𝑤𝜑
srepdf.3	⊢ Ⅎ𝑥𝜑
srepdf.4	⊢ Ⅎ𝑦𝜑
srepdf.5	⊢ Ⅎ𝑧𝜑
srepdf.6	⊢ (𝜑 → ∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)))))

Assertion

Ref	Expression
srepdf	⊢ (𝜑 → ∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓))))

Distinct variable groups:   𝑤,𝑓,𝑥,𝑦,𝑧   𝑓,𝑀,𝑤,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥, 𝑦, 𝑧, 𝑤, 𝑓)   𝜓(𝑥, 𝑦, 𝑧, 𝑤, 𝑓)   𝑀(𝑥)

Proof of Theorem srepdf

Dummy variable 𝑔 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		srepdf.3	. 2 ⊢ Ⅎ𝑥𝜑
2		ax-5 1942	. . 3 ⊢ (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦) → ∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦))
3		nfv 1946	. . . . . 6 ⊢ Ⅎ𝑔(𝜑 ∧ 𝑥 ∈ 𝑀)
4		nfa1 2187	. . . . . 6 ⊢ Ⅎ𝑔∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)
5	3, 4	nfan 1931	. . . . 5 ⊢ Ⅎ𝑔((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦))
6		srepdf.2	. . . . . . 7 ⊢ Ⅎ𝑤𝜑
7		nfv 1946	. . . . . . 7 ⊢ Ⅎ𝑤 𝑥 ∈ 𝑀
8	6, 7	nfan 1931	. . . . . 6 ⊢ Ⅎ𝑤(𝜑 ∧ 𝑥 ∈ 𝑀)
9		nfra1 3286	. . . . . . 7 ⊢ Ⅎ𝑤∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)
10	9	nfal 2353	. . . . . 6 ⊢ Ⅎ𝑤∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)
11	8, 10	nfan 1931	. . . . 5 ⊢ Ⅎ𝑤((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦))
12		srepdf.4	. . . . . . 7 ⊢ Ⅎ𝑦𝜑
13		nfv 1946	. . . . . . 7 ⊢ Ⅎ𝑦 𝑥 ∈ 𝑀
14	12, 13	nfan 1931	. . . . . 6 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑥 ∈ 𝑀)
15		nfcv 2922	. . . . . . . 8 ⊢ Ⅎ𝑦𝑀
16		nfre1 3287	. . . . . . . 8 ⊢ Ⅎ𝑦∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)
17	15, 16	nfralw 3309	. . . . . . 7 ⊢ Ⅎ𝑦∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)
18	17	nfal 2353	. . . . . 6 ⊢ Ⅎ𝑦∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)
19	14, 18	nfan 1931	. . . . 5 ⊢ Ⅎ𝑦((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦))
20		srepdf.5	. . . . . . 7 ⊢ Ⅎ𝑧𝜑
21		nfv 1946	. . . . . . 7 ⊢ Ⅎ𝑧 𝑥 ∈ 𝑀
22	20, 21	nfan 1931	. . . . . 6 ⊢ Ⅎ𝑧(𝜑 ∧ 𝑥 ∈ 𝑀)
23		nfcv 2922	. . . . . . . 8 ⊢ Ⅎ𝑧𝑀
24		nfra1 3286	. . . . . . . . 9 ⊢ Ⅎ𝑧∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)
25	23, 24	nfrexw 3310	. . . . . . . 8 ⊢ Ⅎ𝑧∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)
26	23, 25	nfralw 3309	. . . . . . 7 ⊢ Ⅎ𝑧∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)
27	26	nfal 2353	. . . . . 6 ⊢ Ⅎ𝑧∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)
28	22, 27	nfan 1931	. . . . 5 ⊢ Ⅎ𝑧((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦))
29		simplr 781	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)) → 𝑥 ∈ 𝑀)
30		srepdf.1	. . . . . . . . . 10 ⊢ Ⅎ𝑓𝜑
31		srepdf.6	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)))))
32	30, 31	alrimi 2249	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑓∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)))))
33		funeq 6559	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (Fun 𝑓 ↔ Fun 𝑔))
34		dmeq 5884	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = 𝑔 → dom 𝑓 = dom 𝑔)
35	34	eleq2d 2846	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑤 ∈ dom 𝑓 ↔ 𝑤 ∈ dom 𝑔))
36		fveq1 6884	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑤) = (𝑔‘𝑤))
37	36	eqeq1d 2762	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → ((𝑓‘𝑤) = 𝑧 ↔ (𝑔‘𝑤) = 𝑧))
38	33, 35, 37	3anbi123d 1464	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → ((Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) ↔ (Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧)))
39	38	albidv 1952	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) ↔ ∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧)))
40	39	imbi1d 344	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → ((∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦) ↔ (∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧) → 𝑧 = 𝑦)))
41	40	rexralbidv 3228	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → (∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦) ↔ ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧) → 𝑧 = 𝑦)))
42	41	ralbidv 3185	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦) ↔ ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧) → 𝑧 = 𝑦)))
43	39	anbi2d 642	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → ((𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)) ↔ (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧))))
44	43	rexbidv 3186	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → (∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)) ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧))))
45	44	bibi2d 345	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → ((𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧))) ↔ (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧)))))
46	45	rexralbidv 3228	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → (∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧))) ↔ ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧)))))
47	42, 46	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → ((∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)))) ↔ (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧))))))
48	47	ralbidv 3185	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → (∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)))) ↔ ∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧))))))
49	48	cbvalvw 2068	. . . . . . . . 9 ⊢ (∀𝑓∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)))) ↔ ∀𝑔∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧)))))
50	32, 49	sylib 221	. . . . . . . 8 ⊢ (𝜑 → ∀𝑔∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧)))))
51	50	19.21bi 2225	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧)))))
52	51	r19.21bi 3254	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧)))))
53	52	adantr 486	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)) → (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧)))))
54		simpr 490	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)) → ∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦))
55	54	19.21bi 2225	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)) → ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦))
56		eqid 2760	. . . . 5 ⊢ ({⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)} ↾ 𝑥) = ({⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)} ↾ 𝑥)
57		eqid 2760	. . . . 5 ⊢ {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)} = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)}
58	5, 11, 19, 28, 29, 53, 55, 56, 57	srepdflem2 36005	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓)))
59	58	ex 418	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → (∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓))))
60	2, 59	syl5 35	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓))))
61	1, 60	ralrimia 3261	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103  ∀wal 1567   = wceq 1569  Ⅎwnf 1815   ∈ wcel 2144  ∀wral 3076  ∃wrex 3086  {copab 5166  dom cdm 5650   ↾ cres 5652  Fun wfun 6532  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546

This theorem is used by:  smrepsrep  36007