Theorem srepdf 36087

Description: Derive the strong version of the Axiom Scheme of Replacement used in wfaxrep 46179 (see comments there) from a particular instance of that version of Replacement. Note that this theorem depends on ax-rep 5235, so it does not follow that we could replace ax-rep 5235 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 1945	. . 3 ⊢ (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦) → ∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦))
3		nfv 1949	. . . . . 6 ⊢ Ⅎ𝑔(𝜑 ∧ 𝑥 ∈ 𝑀)
4		nfa1 2191	. . . . . 6 ⊢ Ⅎ𝑔∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)
5	3, 4	nfan 1934	. . . . 5 ⊢ Ⅎ𝑔((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦))
6		srepdf.2	. . . . . . 7 ⊢ Ⅎ𝑤𝜑
7		nfv 1949	. . . . . . 7 ⊢ Ⅎ𝑤 𝑥 ∈ 𝑀
8	6, 7	nfan 1934	. . . . . 6 ⊢ Ⅎ𝑤(𝜑 ∧ 𝑥 ∈ 𝑀)
9		nfra1 3290	. . . . . . 7 ⊢ Ⅎ𝑤∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)
10	9	nfal 2357	. . . . . 6 ⊢ Ⅎ𝑤∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)
11	8, 10	nfan 1934	. . . . 5 ⊢ Ⅎ𝑤((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦))
12		srepdf.4	. . . . . . 7 ⊢ Ⅎ𝑦𝜑
13		nfv 1949	. . . . . . 7 ⊢ Ⅎ𝑦 𝑥 ∈ 𝑀
14	12, 13	nfan 1934	. . . . . 6 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑥 ∈ 𝑀)
15		nfcv 2926	. . . . . . . 8 ⊢ Ⅎ𝑦𝑀
16		nfre1 3291	. . . . . . . 8 ⊢ Ⅎ𝑦∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)
17	15, 16	nfralw 3313	. . . . . . 7 ⊢ Ⅎ𝑦∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)
18	17	nfal 2357	. . . . . 6 ⊢ Ⅎ𝑦∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)
19	14, 18	nfan 1934	. . . . 5 ⊢ Ⅎ𝑦((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦))
20		srepdf.5	. . . . . . 7 ⊢ Ⅎ𝑧𝜑
21		nfv 1949	. . . . . . 7 ⊢ Ⅎ𝑧 𝑥 ∈ 𝑀
22	20, 21	nfan 1934	. . . . . 6 ⊢ Ⅎ𝑧(𝜑 ∧ 𝑥 ∈ 𝑀)
23		nfcv 2926	. . . . . . . 8 ⊢ Ⅎ𝑧𝑀
24		nfra1 3290	. . . . . . . . 9 ⊢ Ⅎ𝑧∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)
25	23, 24	nfrexw 3314	. . . . . . . 8 ⊢ Ⅎ𝑧∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)
26	23, 25	nfralw 3313	. . . . . . 7 ⊢ Ⅎ𝑧∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)
27	26	nfal 2357	. . . . . 6 ⊢ Ⅎ𝑧∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)
28	22, 27	nfan 1934	. . . . 5 ⊢ Ⅎ𝑧((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦))
29		simplr 781	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)) → 𝑥 ∈ 𝑀)
30		srepdf.1	. . . . . . . . . 10 ⊢ Ⅎ𝑓𝜑
31		srepdf.6	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)))))
32	30, 31	alrimi 2253	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑓∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)))))
33		funeq 6579	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (Fun 𝑓 ↔ Fun 𝑔))
34		dmeq 5892	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = 𝑔 → dom 𝑓 = dom 𝑔)
35	34	eleq2d 2850	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑤 ∈ dom 𝑓 ↔ 𝑤 ∈ dom 𝑔))
36		fveq1 6907	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑤) = (𝑔‘𝑤))
37	36	eqeq1d 2765	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → ((𝑓‘𝑤) = 𝑧 ↔ (𝑔‘𝑤) = 𝑧))
38	33, 35, 37	3anbi123d 1465	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → ((Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) ↔ (Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧)))
39	38	albidv 1955	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) ↔ ∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧)))
40	39	imbi1d 344	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → ((∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦) ↔ (∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧) → 𝑧 = 𝑦)))
41	40	rexralbidv 3232	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → (∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦) ↔ ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧) → 𝑧 = 𝑦)))
42	41	ralbidv 3189	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦) ↔ ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧) → 𝑧 = 𝑦)))
43	39	anbi2d 642	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → ((𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)) ↔ (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧))))
44	43	rexbidv 3190	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → (∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)) ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧))))
45	44	bibi2d 345	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → ((𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧))) ↔ (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧)))))
46	45	rexralbidv 3232	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → (∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧))) ↔ ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧)))))
47	42, 46	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → ((∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)))) ↔ (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧))))))
48	47	ralbidv 3189	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → (∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)))) ↔ ∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧))))))
49	48	cbvalvw 2071	. . . . . . . . 9 ⊢ (∀𝑓∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)))) ↔ ∀𝑔∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧)))))
50	32, 49	sylib 221	. . . . . . . 8 ⊢ (𝜑 → ∀𝑔∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧)))))
51	50	19.21bi 2229	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧)))))
52	51	r19.21bi 3258	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧)))))
53	52	adantr 486	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)) → (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ (𝑔‘𝑤) = 𝑧)))))
54		simpr 490	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)) → ∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦))
55	54	19.21bi 2229	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)) → ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦))
56		eqid 2763	. . . . 5 ⊢ ({⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)} ↾ 𝑥) = ({⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)} ↾ 𝑥)
57		eqid 2763	. . . . 5 ⊢ {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)} = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)}
58	5, 11, 19, 28, 29, 53, 55, 56, 57	srepdflem2 36086	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦)) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓)))
59	58	ex 418	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → (∀𝑔∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓))))
60	2, 59	syl5 35	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓))))
61	1, 60	ralrimia 3265	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103  ∀wal 1568   = wceq 1570  Ⅎwnf 1816   ∈ wcel 2147  ∀wral 3080  ∃wrex 3090  {copab 5170  dom cdm 5655   ↾ cres 5657  Fun wfun 6552  ‘cfv 6558

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566

This theorem is used by:  smrepsrep  36088