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	⊢ Ⅎ 𝑥 𝜑
	nfcdeq.2	⊢ CondEq ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	nfcdeq	⊢ ( 𝜑 ↔ 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		nfcdeq.1	⊢ Ⅎ 𝑥 𝜑
2		nfcdeq.2	⊢ CondEq ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
3	1	sbf	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜑 )
4		nfv	⊢ Ⅎ 𝑥 𝜓
5	2	cdeqri	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
6	4 5	sbie	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 )
7	3 6	bitr3i	⊢ ( 𝜑 ↔ 𝜓 )