Theorem cbvex2
Rule used to change bound variables, using implicit substitution. Usage
of this theorem is discouraged because it depends on [ax-13]. Use the
weaker cbvex2v if possible. (Contributed by NM, 14-Sep-2003.)
(Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf
Lammen, 16-Jun-2019.) (New usage is discouraged.)
Hypotheses
cbval2.1
\( \vdash \Finv z \, \varphi \)
cbval2.2
\( \vdash \Finv w \, \varphi \)
cbval2.3
\( \vdash \Finv x \, \psi \)
cbval2.4
\( \vdash \Finv y \, \psi \)
cbval2.5
\( \vdash x = z \wedge y = w \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \exists x \, \exists y \, \varphi \leftrightarrow \exists z \, \exists w \, \psi \)
Proof
cbval2.1
l1
nfn _
cbval2.2
l3
nfn _
cbval2.3
l5
nfn _
cbval2.4
l7
nfn _
cbval2.5
notbid _
l10
cbval2 l1 l3 l5 l7 _
\( \vdash \forall x \, \forall y \, \neg \varphi \leftrightarrow \forall z \, \forall w \, \neg \psi \)
l11
2nexaln
\( \vdash \neg \exists x \, \exists y \, \varphi \leftrightarrow \forall x \, \forall y \, \neg \varphi \)
2nexaln
\( \vdash \neg \exists z \, \exists w \, \psi \leftrightarrow \forall z \, \forall w \, \neg \psi \)
3bitr4i l10 l11 _
con4bii _