Theorem bj-nfcsym 32886

Description: The class-form not-free predicate defines a symmetric binary relation on var metavariables (irreflexivity is proved by nfnid 4897 with additional axioms; see also nfcv 2764). This could be proved from aecom 2311 and nfcvb 4898 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 2628 instead of equcomd 1946; removing dependency on ax-ext 2602 is possible: prove weak versions (i.e. replace classes with setvars) of drnfc1 2782, eleq2d 2687 (using elequ2 2004), nfcvf 2788, dvelimc 2787, dvelimdc 2786, nfcvf2 2789. (Proof modification is discouraged.)

Assertion

Ref	Expression
bj-nfcsym	|- ( F/_ x y <-> F/_ y x )

Proof of Theorem bj-nfcsym

Step	Hyp	Ref	Expression
1		sp 2053	. . . 4 |- ( A. x x = y -> x = y )
2	1	equcomd 1946	. . 3 |- ( A. x x = y -> y = x )
3	2	drnfc1 2782	. 2 |- ( A. x x = y -> ( F/_ x y <-> F/_ y x ) )
4		nfcvf 2788	. . 3 |- ( -. A. x x = y -> F/_ x y )
5		nfcvf2 2789	. . 3 |- ( -. A. x x = y -> F/_ y x )
6	4, 5	2thd 255	. 2 |- ( -. A. x x = y -> ( F/_ x y <-> F/_ y x ) )
7	3, 6	pm2.61i 176	1 |- ( F/_ x y <-> F/_ y x )

Syntax hints:   -. wn 3   <-> wb 196   A.wal 1481   F/_wnfc 2751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-cleq 2615  df-clel 2618  df-nfc 2753

This theorem is referenced by: (None)