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	|- F/ x ph
	nfcdeq.2	|- CondEq ( x = y -> ( ph <-> ps ) )
Assertion	nfcdeq	|- ( ph <-> ps )

Proof

Step	Hyp	Ref	Expression
1		nfcdeq.1	|- F/ x ph
2		nfcdeq.2	|- CondEq ( x = y -> ( ph <-> ps ) )
3	1	sbf	|- ( [ y / x ] ph <-> ph )
4		nfv	|- F/ x ps
5	2	cdeqri	|- ( x = y -> ( ph <-> ps ) )
6	4 5	sbie	|- ( [ y / x ] ph <-> ps )
7	3 6	bitr3i	|- ( ph <-> ps )