Theorem bj-nfcsym

Description: The nonfreeness quantifier for classes defines a symmetric binary relation on var metavariables (irreflexivity is proved by nfnid with additional axioms; see also nfcv ). This could be proved from aecom and nfcvb but the latter requires a domain with at least two objects (hence uses extra axioms). (Contributed by BJ, 30-Sep-2018) Proof modification is discouraged to avoid use of eqcomd instead of equcomd ; removing dependency on ax-ext is possible: prove weak versions (i.e. replace classes with setvars) of drnfc1 , eleq2d (using elequ2 ), nfcvf , dvelimc , dvelimdc , nfcvf2 . (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-nfcsym	$$⊢\underset{\_}{Ⅎ}xy\leftrightarrow \underset{\_}{Ⅎ}yx$$

Proof

Step	Hyp	Ref	Expression
1		sp	$$⊢\forall xx=y\to x=y$$
2	1	equcomd	$$⊢\forall xx=y\to y=x$$
3	2	drnfc1	$$⊢\forall xx=y\to \left(\underset{\_}{Ⅎ}xy\leftrightarrow \underset{\_}{Ⅎ}yx\right)$$
4		nfcvf	$$⊢\neg \forall xx=y\to \underset{\_}{Ⅎ}xy$$
5		nfcvf2	$$⊢\neg \forall xx=y\to \underset{\_}{Ⅎ}yx$$
6	4 5	2thd	$$⊢\neg \forall xx=y\to \left(\underset{\_}{Ⅎ}xy\leftrightarrow \underset{\_}{Ⅎ}yx\right)$$
7	3 6	pm2.61i	$$⊢\underset{\_}{Ⅎ}xy\leftrightarrow \underset{\_}{Ⅎ}yx$$