Theorem ax12wdemo
Example of an application of ax12w that results in an instance of
[ax-12] for a contrived formula with mixed free and bound variables,
\( x \in y \wedge \forall x \, z \in x \wedge \forall y \, \forall z \, y \in x \), in place of \( \varphi \).
The proof illustrates bound variable renaming with cbvalvw to obtain
fresh variables to avoid distinct variable clashes. Uses only Tarski's
FOL axiom schemes. (Contributed by NM, 14-Apr-2017.)
Conclusion
\( \vdash x = y \rightarrow \forall y \, (x \in y \wedge \forall x \, z \in x \wedge \forall y \, \forall z \, y \in x) \rightarrow \forall x \, (x = y \rightarrow x \in y \wedge \forall x \, z \in x \wedge \forall y \, \forall z \, y \in x) \)
Proof
l0
elequ1
elequ2
cbvalvw _
l3
a1i _
elequ1
albidv _
l6
cbvalvw _
\( \vdash \forall y \, \forall z \, y \in x \leftrightarrow \forall v \, \forall z \, v \in x \)
elequ2
albidv _
albidv _
\( \vdash x = y \rightarrow (\forall v \, \forall z \, v \in x \leftrightarrow \forall v \, \forall z \, v \in y) \)
bitrid l6 _
l11
3anbi123d l0 l3 _
\( \vdash x = y \rightarrow (x \in y \wedge \forall x \, z \in x \wedge \forall y \, \forall z \, y \in x \leftrightarrow y \in y \wedge \forall w \, z \in w \wedge \forall v \, \forall z \, v \in y) \)
l12
elequ2
a1i l6
3anbi13d l12 _
\( \vdash y = v \rightarrow (x \in y \wedge \forall x \, z \in x \wedge \forall y \, \forall z \, y \in x \leftrightarrow x \in v \wedge \forall x \, z \in x \wedge \forall v \, \forall z \, v \in x) \)
ax12w l11 _