Theorem nfceqiOLD

Description: Obsolete proof of nfceqi as of 19-Jun-2023. (Contributed by Mario Carneiro, 11-Aug-2016) (Proof shortened by Wolf Lammen, 16-Nov-2019) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	nfcxfr.1	$$⊢A=B$$
Assertion	nfceqiOLD	$$⊢\underset{\_}{Ⅎ}xA\leftrightarrow \underset{\_}{Ⅎ}xB$$

Proof

Step	Hyp	Ref	Expression
1		nfcxfr.1	$$⊢A=B$$
2		nftru	$$⊢Ⅎx\top$$
3	1	a1i	$$⊢\top \to A=B$$
4	2 3	nfceqdf	$$⊢\top \to \left(\underset{\_}{Ⅎ}xA\leftrightarrow \underset{\_}{Ⅎ}xB\right)$$
5	4	mptru	$$⊢\underset{\_}{Ⅎ}xA\leftrightarrow \underset{\_}{Ⅎ}xB$$