Theorem bj-nfcsym 36887

Description: The nonfreeness quantifier for classes defines a symmetric binary relation on var metavariables (irreflexivity is proved by nfnid 5330 with additional axioms; see also nfcv 2891). This could be proved from aecom 2425 and nfcvb 5331 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 2735 instead of equcomd 2019; removing dependency on ax-ext 2701 is possible: prove weak versions (i.e. replace classes with setvars) of drnfc1 2911, eleq2d 2814 (using elequ2 2124), nfcvf 2918, dvelimc 2917, dvelimdc 2916, nfcvf2 2919. (Proof modification is discouraged.)

Assertion

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

Proof of Theorem bj-nfcsym

Step	Hyp	Ref	Expression
1		sp 2184	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)
2	1	equcomd 2019	. . 3 ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑦 = 𝑥)
3	2	drnfc1 2911	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝑦 ↔ Ⅎ𝑦𝑥))
4		nfcvf 2918	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦)
5		nfcvf2 2919	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥)
6	4, 5	2thd 265	. 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝑦 ↔ Ⅎ𝑦𝑥))
7	3, 6	pm2.61i 182	1 ⊢ (Ⅎ𝑥𝑦 ↔ Ⅎ𝑦𝑥)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1538  Ⅎwnfc 2876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-13 2370  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2721  df-nfc 2878

This theorem is referenced by: (None)