Theorem bj-nfcsym 35779

Description: The nonfreeness quantifier for classes defines a symmetric binary relation on var metavariables (irreflexivity is proved by nfnid 5374 with additional axioms; see also nfcv 2904). This could be proved from aecom 2427 and nfcvb 5375 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 2739 instead of equcomd 2023; removing dependency on ax-ext 2704 is possible: prove weak versions (i.e. replace classes with setvars) of drnfc1 2923, eleq2d 2820 (using elequ2 2122), nfcvf 2933, dvelimc 2932, dvelimdc 2931, nfcvf2 2934. (Proof modification is discouraged.)

Assertion

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

Proof of Theorem bj-nfcsym

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

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1540  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-13 2372  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-cleq 2725  df-nfc 2886

This theorem is referenced by: (None)