Theorem nfcdeq

Description: If we have a conditional equality proof, where ph is ph ( x ) and ps is ph ( y ) , and ph ( x ) in fact does not have x free in it according to F/ , then ph ( x ) <-> ph ( y ) unconditionally. This proves that F/ x ph is actually a not-free predicate. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Mario Carneiro, 11-Aug-2016) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nfcdeq.1	$$⊢Ⅎx\phi$$
	nfcdeq.2	$$⊢CondEq\left(x=y\to \left(\phi \leftrightarrow \psi \right)\right)$$
Assertion	nfcdeq	$$⊢\phi \leftrightarrow \psi$$

Proof

Step	Hyp	Ref	Expression
1		nfcdeq.1	$$⊢Ⅎx\phi$$
2		nfcdeq.2	$$⊢CondEq\left(x=y\to \left(\phi \leftrightarrow \psi \right)\right)$$
3	1	sbf	$$⊢\left[y/x\right]\phi \leftrightarrow \phi$$
4		nfv	$$⊢Ⅎx\psi$$
5	2	cdeqri	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
6	4 5	sbie	$$⊢\left[y/x\right]\phi \leftrightarrow \psi$$
7	3 6	bitr3i	$$⊢\phi \leftrightarrow \psi$$