Theorem nfcjust

Description: Justification theorem for df-nfc . (Contributed by Mario Carneiro, 13-Oct-2016)

	Ref	Expression
Assertion	nfcjust	$$⊢\forall yℲxy\in A\leftrightarrow \forall zℲxz\in A$$

Proof

Step	Hyp	Ref	Expression
1		eleq1w	$$⊢y=z\to \left(y\in A\leftrightarrow z\in A\right)$$
2	1	nfbidv	$$⊢y=z\to \left(Ⅎxy\in A\leftrightarrow Ⅎxz\in A\right)$$
3	2	cbvalvw	$$⊢\forall yℲxy\in A\leftrightarrow \forall zℲxz\in A$$