Theorem bj-nfcsym 37043

Description: The nonfreeness quantifier for classes defines a symmetric binary relation on var metavariables (irreflexivity is proved by nfnid 5318 with additional axioms; see also nfcv 2896). This could be proved from aecom 2429 and nfcvb 5319 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 2740 instead of equcomd 2020; removing dependency on ax-ext 2706 is possible: prove weak versions (i.e. replace classes with setvars) of drnfc1 2916, eleq2d 2820 (using elequ2 2128), nfcvf 2923, dvelimc 2922, dvelimdc 2921, nfcvf2 2924. (Proof modification is discouraged.)

Assertion

Ref	Expression
bj-nfcsym	⊢ (Ⅎ𝑥𝑦 ↔ Ⅎ𝑦𝑥)

Proof of Theorem bj-nfcsym

Step	Hyp	Ref	Expression
1		sp 2188	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)
2	1	equcomd 2020	. . 3 ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑦 = 𝑥)
3	2	drnfc1 2916	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝑦 ↔ Ⅎ𝑦𝑥))
4		nfcvf 2923	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦)
5		nfcvf2 2924	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥)
6	4, 5	2thd 265	. 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝑦 ↔ Ⅎ𝑦𝑥))
7	3, 6	pm2.61i 182	1 ⊢ (Ⅎ𝑥𝑦 ↔ Ⅎ𝑦𝑥)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1539  Ⅎwnfc 2881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-13 2374  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-cleq 2726  df-nfc 2883

This theorem is referenced by: (None)