Theorem nfceqi

Description: Equality theorem for class not-free. (Contributed by Mario Carneiro, 11-Aug-2016) (Proof shortened by Wolf Lammen, 16-Nov-2019) Avoid ax-12 . (Revised by Wolf Lammen, 19-Jun-2023)

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

Proof

Step	Hyp	Ref	Expression
1		nfceqi.1	$$⊢A=B$$
2	1	eleq2i	$$⊢y\in A\leftrightarrow y\in B$$
3	2	nfbii	$$⊢Ⅎxy\in A\leftrightarrow Ⅎxy\in B$$
4	3	albii	$$⊢\forall yℲxy\in A\leftrightarrow \forall yℲxy\in B$$
5		df-nfc	$$⊢\underset{\_}{Ⅎ}xA\leftrightarrow \forall yℲxy\in A$$
6		df-nfc	$$⊢\underset{\_}{Ⅎ}xB\leftrightarrow \forall yℲxy\in B$$
7	4 5 6	3bitr4i	$$⊢\underset{\_}{Ⅎ}xA\leftrightarrow \underset{\_}{Ⅎ}xB$$