Metamath Proof Explorer

Theorem srepdf

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

Ref Expression
Hypotheses srepdf.1 ⊢ Ⅎ f φ
srepdf.2 ⊢ Ⅎ w φ
srepdf.3 ⊢ Ⅎ x φ
srepdf.4 ⊢ Ⅎ y φ
srepdf.5 ⊢ Ⅎ z φ
srepdf.6 ⊢ φ → ∀ x ∈ M ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y Fun ⁡ f ∧ w ∈ dom ⁡ f ∧ f ⁡ w = z → z = y → ∃ y ∈ M ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y Fun ⁡ f ∧ w ∈ dom ⁡ f ∧ f ⁡ w = z
Assertion srepdf ⊢ φ → ∀ x ∈ M ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y ψ → z = y → ∃ y ∈ M ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y ψ

Proof

Step Hyp Ref Expression
1 srepdf.1 ⊢ Ⅎ f φ
2 srepdf.2 ⊢ Ⅎ w φ
3 srepdf.3 ⊢ Ⅎ x φ
4 srepdf.4 ⊢ Ⅎ y φ
5 srepdf.5 ⊢ Ⅎ z φ
6 srepdf.6 ⊢ φ → ∀ x ∈ M ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y Fun ⁡ f ∧ w ∈ dom ⁡ f ∧ f ⁡ w = z → z = y → ∃ y ∈ M ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y Fun ⁡ f ∧ w ∈ dom ⁡ f ∧ f ⁡ w = z
7 ax-5 ⊢ ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y ψ → z = y → ∀ g ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y ψ → z = y
8 nfv ⊢ Ⅎ g φ ∧ x ∈ M
9 nfa1 ⊢ Ⅎ g ∀ g ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y ψ → z = y
10 8 9 nfan ⊢ Ⅎ g φ ∧ x ∈ M ∧ ∀ g ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y ψ → z = y
11 nfv ⊢ Ⅎ w x ∈ M
12 2 11 nfan ⊢ Ⅎ w φ ∧ x ∈ M
13 nfra1 ⊢ Ⅎ w ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y ψ → z = y
14 13 nfal ⊢ Ⅎ w ∀ g ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y ψ → z = y
15 12 14 nfan ⊢ Ⅎ w φ ∧ x ∈ M ∧ ∀ g ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y ψ → z = y
16 nfv ⊢ Ⅎ y x ∈ M
17 4 16 nfan ⊢ Ⅎ y φ ∧ x ∈ M
18 nfcv ⊢ Ⅎ _ y M
19 nfre1 ⊢ Ⅎ y ∃ y ∈ M ∀ z ∈ M ∀ y ψ → z = y
20 18 19 nfralw ⊢ Ⅎ y ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y ψ → z = y
21 20 nfal ⊢ Ⅎ y ∀ g ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y ψ → z = y
22 17 21 nfan ⊢ Ⅎ y φ ∧ x ∈ M ∧ ∀ g ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y ψ → z = y
23 nfv ⊢ Ⅎ z x ∈ M
24 5 23 nfan ⊢ Ⅎ z φ ∧ x ∈ M
25 nfcv ⊢ Ⅎ _ z M
26 nfra1 ⊢ Ⅎ z ∀ z ∈ M ∀ y ψ → z = y
27 25 26 nfrexw ⊢ Ⅎ z ∃ y ∈ M ∀ z ∈ M ∀ y ψ → z = y
28 25 27 nfralw ⊢ Ⅎ z ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y ψ → z = y
29 28 nfal ⊢ Ⅎ z ∀ g ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y ψ → z = y
30 24 29 nfan ⊢ Ⅎ z φ ∧ x ∈ M ∧ ∀ g ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y ψ → z = y
31 simplr ⊢ φ ∧ x ∈ M ∧ ∀ g ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y ψ → z = y → x ∈ M
32 1 6 alrimi ⊢ φ → ∀ f ∀ x ∈ M ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y Fun ⁡ f ∧ w ∈ dom ⁡ f ∧ f ⁡ w = z → z = y → ∃ y ∈ M ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y Fun ⁡ f ∧ w ∈ dom ⁡ f ∧ f ⁡ w = z
33 funeq ⊢ f = g → Fun ⁡ f ↔ Fun ⁡ g
34 dmeq ⊢ f = g → dom ⁡ f = dom ⁡ g
35 34 eleq2d ⊢ f = g → w ∈ dom ⁡ f ↔ w ∈ dom ⁡ g
36 fveq1 ⊢ f = g → f ⁡ w = g ⁡ w
37 36 eqeq1d ⊢ f = g → f ⁡ w = z ↔ g ⁡ w = z
38 33 35 37 3anbi123d ⊢ f = g → Fun ⁡ f ∧ w ∈ dom ⁡ f ∧ f ⁡ w = z ↔ Fun ⁡ g ∧ w ∈ dom ⁡ g ∧ g ⁡ w = z
39 38 albidv ⊢ f = g → ∀ y Fun ⁡ f ∧ w ∈ dom ⁡ f ∧ f ⁡ w = z ↔ ∀ y Fun ⁡ g ∧ w ∈ dom ⁡ g ∧ g ⁡ w = z
40 39 imbi1d ⊢ f = g → ∀ y Fun ⁡ f ∧ w ∈ dom ⁡ f ∧ f ⁡ w = z → z = y ↔ ∀ y Fun ⁡ g ∧ w ∈ dom ⁡ g ∧ g ⁡ w = z → z = y
41 40 rexralbidv ⊢ f = g → ∃ y ∈ M ∀ z ∈ M ∀ y Fun ⁡ f ∧ w ∈ dom ⁡ f ∧ f ⁡ w = z → z = y ↔ ∃ y ∈ M ∀ z ∈ M ∀ y Fun ⁡ g ∧ w ∈ dom ⁡ g ∧ g ⁡ w = z → z = y
42 41 ralbidv ⊢ f = g → ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y Fun ⁡ f ∧ w ∈ dom ⁡ f ∧ f ⁡ w = z → z = y ↔ ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y Fun ⁡ g ∧ w ∈ dom ⁡ g ∧ g ⁡ w = z → z = y
43 39 anbi2d ⊢ f = g → w ∈ x ∧ ∀ y Fun ⁡ f ∧ w ∈ dom ⁡ f ∧ f ⁡ w = z ↔ w ∈ x ∧ ∀ y Fun ⁡ g ∧ w ∈ dom ⁡ g ∧ g ⁡ w = z
44 43 rexbidv ⊢ f = g → ∃ w ∈ M w ∈ x ∧ ∀ y Fun ⁡ f ∧ w ∈ dom ⁡ f ∧ f ⁡ w = z ↔ ∃ w ∈ M w ∈ x ∧ ∀ y Fun ⁡ g ∧ w ∈ dom ⁡ g ∧ g ⁡ w = z
45 44 bibi2d ⊢ f = g → z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y Fun ⁡ f ∧ w ∈ dom ⁡ f ∧ f ⁡ w = z ↔ z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y Fun ⁡ g ∧ w ∈ dom ⁡ g ∧ g ⁡ w = z
46 45 rexralbidv ⊢ f = g → ∃ y ∈ M ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y Fun ⁡ f ∧ w ∈ dom ⁡ f ∧ f ⁡ w = z ↔ ∃ y ∈ M ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y Fun ⁡ g ∧ w ∈ dom ⁡ g ∧ g ⁡ w = z
47 42 46 imbi12d ⊢ f = g → ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y Fun ⁡ f ∧ w ∈ dom ⁡ f ∧ f ⁡ w = z → z = y → ∃ y ∈ M ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y Fun ⁡ f ∧ w ∈ dom ⁡ f ∧ f ⁡ w = z ↔ ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y Fun ⁡ g ∧ w ∈ dom ⁡ g ∧ g ⁡ w = z → z = y → ∃ y ∈ M ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y Fun ⁡ g ∧ w ∈ dom ⁡ g ∧ g ⁡ w = z
48 47 ralbidv ⊢ f = g → ∀ x ∈ M ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y Fun ⁡ f ∧ w ∈ dom ⁡ f ∧ f ⁡ w = z → z = y → ∃ y ∈ M ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y Fun ⁡ f ∧ w ∈ dom ⁡ f ∧ f ⁡ w = z ↔ ∀ x ∈ M ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y Fun ⁡ g ∧ w ∈ dom ⁡ g ∧ g ⁡ w = z → z = y → ∃ y ∈ M ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y Fun ⁡ g ∧ w ∈ dom ⁡ g ∧ g ⁡ w = z
49 48 cbvalvw ⊢ ∀ f ∀ x ∈ M ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y Fun ⁡ f ∧ w ∈ dom ⁡ f ∧ f ⁡ w = z → z = y → ∃ y ∈ M ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y Fun ⁡ f ∧ w ∈ dom ⁡ f ∧ f ⁡ w = z ↔ ∀ g ∀ x ∈ M ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y Fun ⁡ g ∧ w ∈ dom ⁡ g ∧ g ⁡ w = z → z = y → ∃ y ∈ M ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y Fun ⁡ g ∧ w ∈ dom ⁡ g ∧ g ⁡ w = z
50 32 49 sylib ⊢ φ → ∀ g ∀ x ∈ M ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y Fun ⁡ g ∧ w ∈ dom ⁡ g ∧ g ⁡ w = z → z = y → ∃ y ∈ M ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y Fun ⁡ g ∧ w ∈ dom ⁡ g ∧ g ⁡ w = z
51 50 19.21bi ⊢ φ → ∀ x ∈ M ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y Fun ⁡ g ∧ w ∈ dom ⁡ g ∧ g ⁡ w = z → z = y → ∃ y ∈ M ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y Fun ⁡ g ∧ w ∈ dom ⁡ g ∧ g ⁡ w = z
52 51 r19.21bi ⊢ φ ∧ x ∈ M → ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y Fun ⁡ g ∧ w ∈ dom ⁡ g ∧ g ⁡ w = z → z = y → ∃ y ∈ M ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y Fun ⁡ g ∧ w ∈ dom ⁡ g ∧ g ⁡ w = z
53 52 adantr ⊢ φ ∧ x ∈ M ∧ ∀ g ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y ψ → z = y → ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y Fun ⁡ g ∧ w ∈ dom ⁡ g ∧ g ⁡ w = z → z = y → ∃ y ∈ M ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y Fun ⁡ g ∧ w ∈ dom ⁡ g ∧ g ⁡ w = z
54 simpr ⊢ φ ∧ x ∈ M ∧ ∀ g ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y ψ → z = y → ∀ g ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y ψ → z = y
55 54 19.21bi ⊢ φ ∧ x ∈ M ∧ ∀ g ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y ψ → z = y → ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y ψ → z = y
56 eqid ⊢ w z | w ∈ M ∧ z ∈ M ∧ ∀ y ψ ↾ x = w z | w ∈ M ∧ z ∈ M ∧ ∀ y ψ ↾ x
57 eqid ⊢ w z | w ∈ M ∧ z ∈ M ∧ ∀ y ψ = w z | w ∈ M ∧ z ∈ M ∧ ∀ y ψ
58 10 15 22 30 31 53 55 56 57 srepdflem2 ⊢ φ ∧ x ∈ M ∧ ∀ g ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y ψ → z = y → ∃ y ∈ M ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y ψ
59 58 ex ⊢ φ ∧ x ∈ M → ∀ g ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y ψ → z = y → ∃ y ∈ M ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y ψ
60 7 59 syl5 ⊢ φ ∧ x ∈ M → ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y ψ → z = y → ∃ y ∈ M ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y ψ
61 3 60 ralrimia ⊢ φ → ∀ x ∈ M ∀ w ∈ M ∃ y ∈ M ∀ z ∈ M ∀ y ψ → z = y → ∃ y ∈ M ∀ z ∈ M z ∈ y ↔ ∃ w ∈ M w ∈ x ∧ ∀ y ψ