Theorem dfnfc2

Description: An alternative statement of the effective freeness of a class A , when it is a set. (Contributed by Mario Carneiro, 14-Oct-2016) (Proof shortened by JJ, 26-Jul-2021)

	Ref	Expression
Assertion	dfnfc2	$$⊢\forall xA\in V\to \left(\underset{\_}{Ⅎ}xA\leftrightarrow \forall yℲxy=A\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfcvd	$$⊢\underset{\_}{Ⅎ}xA\to \underset{\_}{Ⅎ}xy$$
2		id	$$⊢\underset{\_}{Ⅎ}xA\to \underset{\_}{Ⅎ}xA$$
3	1 2	nfeqd	$$⊢\underset{\_}{Ⅎ}xA\to Ⅎxy=A$$
4	3	alrimiv	$$⊢\underset{\_}{Ⅎ}xA\to \forall yℲxy=A$$
5		df-nfc	$$⊢\underset{\_}{Ⅎ}x\left\{A\right\}\leftrightarrow \forall yℲxy\in \left\{A\right\}$$
6		velsn	$$⊢y\in \left\{A\right\}\leftrightarrow y=A$$
7	6	nfbii	$$⊢Ⅎxy\in \left\{A\right\}\leftrightarrow Ⅎxy=A$$
8	7	albii	$$⊢\forall yℲxy\in \left\{A\right\}\leftrightarrow \forall yℲxy=A$$
9	5 8	sylbbr	$$⊢\forall yℲxy=A\to \underset{\_}{Ⅎ}x\left\{A\right\}$$
10	9	nfunid	$$⊢\forall yℲxy=A\to \underset{\_}{Ⅎ}x\bigcup \left\{A\right\}$$
11		nfa1	$$⊢Ⅎx\forall xA\in V$$
12		unisng	$$⊢A\in V\to \bigcup \left\{A\right\}=A$$
13	12	sps	$$⊢\forall xA\in V\to \bigcup \left\{A\right\}=A$$
14	11 13	nfceqdf	$$⊢\forall xA\in V\to \left(\underset{\_}{Ⅎ}x\bigcup \left\{A\right\}\leftrightarrow \underset{\_}{Ⅎ}xA\right)$$
15	10 14	imbitrid	$$⊢\forall xA\in V\to \left(\forall yℲxy=A\to \underset{\_}{Ⅎ}xA\right)$$
16	4 15	impbid2	$$⊢\forall xA\in V\to \left(\underset{\_}{Ⅎ}xA\leftrightarrow \forall yℲxy=A\right)$$