Theorem drnf1v
Formula-building lemma for use with the Distinctor Reduction Theorem.
Version of drnf1 with a disjoint variable condition, which does not
require [ax-13]. (Contributed by Mario Carneiro, 4-Oct-2016.)
(Revised by BJ, 17-Jun-2019.) Avoid [ax-10]. (Revised by GG,
18-Nov-2024.)
Hypothesis
dral1v.1
\( \vdash \forall x \, x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \forall x \, x = y \rightarrow (\Finv x \, \varphi \leftrightarrow \Finv y \, \psi) \)
Proof
dral1v.1
l1
drex1v _
dral1v.1
dral1v _
l4
imbi12d l1 _
\( \vdash \forall x \, x = y \rightarrow (\exists x \, \varphi \rightarrow \forall x \, \varphi \leftrightarrow \exists y \, \psi \rightarrow \forall y \, \psi) \)
l5
df-nf
\( \vdash \Finv x \, \varphi \leftrightarrow \exists x \, \varphi \rightarrow \forall x \, \varphi \)
df-nf
\( \vdash \Finv y \, \psi \leftrightarrow \exists y \, \psi \rightarrow \forall y \, \psi \)
3bitr4g l4 l5 _