Theorem nfeqf
A variable is effectively not free in an equality if it is not either of
the involved variables. F/ version of [ax-c9]. Usage of this
theorem is discouraged because it depends on [ax-13]. (Contributed by
Mario Carneiro, 6-Oct-2016.) Remove dependency on [ax-11]. (Revised
by Wolf Lammen, 6-Sep-2018.) (New usage is discouraged.)
Conclusion
\( \vdash \neg \forall z \, z = x' \wedge \neg \forall z \, z = y' \rightarrow \Finv z \, x' = y' \)
Proof
l0
nfna1
nfna1
l2
nfan l0 _
l3
equvinva
\( \vdash x' = y' \rightarrow \exists w \, (x' = w \wedge y' = w) \)
dveeq1
l5
imp _
\( \vdash \neg \forall z \, z = x' \wedge x' = w \rightarrow \forall z \, x' = w \)
dveeq1
l7
imp _
\( \vdash \neg \forall z \, z = y' \wedge y' = w \rightarrow \forall z \, y' = w \)
equtr2
alanimi _
\( \vdash \forall z \, x' = w \wedge \forall z \, y' = w \rightarrow \forall z \, x' = y' \)
syl2an l5 l7 _
an4s _
ex _
exlimdv _
\( \vdash \neg \forall z \, z = x' \wedge \neg \forall z \, z = y' \rightarrow \exists w \, (x' = w \wedge y' = w) \rightarrow \forall z \, x' = y' \)
syl5 l3 _
nf5d l2 _