Metamath Proof Explorer

Theorem axrep5

Description: Axiom of Replacement (similar to Axiom Rep of BellMachover p. 463). The antecedent tells us ph is analogous to a "function" from x to y (although it is not really a function since it is a wff and not a class). In the consequent we postulate the existence of a set z that corresponds to the "image" of ph restricted to some other set w . The hypothesis says z must not be free in ph . (Contributed by NM, 26-Nov-1995) (Revised by Mario Carneiro, 14-Oct-2016)

Ref Expression
Hypothesis axrep5.1 ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{\phi }$
Assertion axrep5 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\to \exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {y}={z}\right)\right)\to \exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {z}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge {\phi }\right)\right)$

Proof

Step Hyp Ref Expression
1 axrep5.1 ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{\phi }$
2 19.37v ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {y}={z}\right)\right)↔\left({x}\in {w}\to \exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {y}={z}\right)\right)$
3 impexp ${⊢}\left(\left({x}\in {w}\wedge {\phi }\right)\to {y}={z}\right)↔\left({x}\in {w}\to \left({\phi }\to {y}={z}\right)\right)$
4 3 albii ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {w}\wedge {\phi }\right)\to {y}={z}\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\to \left({\phi }\to {y}={z}\right)\right)$
5 19.21v ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\to \left({\phi }\to {y}={z}\right)\right)↔\left({x}\in {w}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {y}={z}\right)\right)$
6 4 5 bitr2i ${⊢}\left({x}\in {w}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {y}={z}\right)\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {w}\wedge {\phi }\right)\to {y}={z}\right)$
7 6 exbii ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {y}={z}\right)\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {w}\wedge {\phi }\right)\to {y}={z}\right)$
8 2 7 bitr3i ${⊢}\left({x}\in {w}\to \exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {y}={z}\right)\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {w}\wedge {\phi }\right)\to {y}={z}\right)$
9 8 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\to \exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {y}={z}\right)\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {w}\wedge {\phi }\right)\to {y}={z}\right)$
10 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{x}\in {w}$
11 10 1 nfan ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge {\phi }\right)$
12 11 axrep4 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {w}\wedge {\phi }\right)\to {y}={z}\right)\to \exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {z}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge \left({x}\in {w}\wedge {\phi }\right)\right)\right)$
13 9 12 sylbi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\to \exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {y}={z}\right)\right)\to \exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {z}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge \left({x}\in {w}\wedge {\phi }\right)\right)\right)$
14 anabs5 ${⊢}\left({x}\in {w}\wedge \left({x}\in {w}\wedge {\phi }\right)\right)↔\left({x}\in {w}\wedge {\phi }\right)$
15 14 exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge \left({x}\in {w}\wedge {\phi }\right)\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge {\phi }\right)$
16 15 bibi2i ${⊢}\left({y}\in {z}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge \left({x}\in {w}\wedge {\phi }\right)\right)\right)↔\left({y}\in {z}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge {\phi }\right)\right)$
17 16 albii ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {z}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge \left({x}\in {w}\wedge {\phi }\right)\right)\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {z}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge {\phi }\right)\right)$
18 17 exbii ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {z}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge \left({x}\in {w}\wedge {\phi }\right)\right)\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {z}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge {\phi }\right)\right)$
19 13 18 sylib ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\to \exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {y}={z}\right)\right)\to \exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {z}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge {\phi }\right)\right)$