Theorem bj-nfcsym 37252

Description: The nonfreeness quantifier for classes defines a symmetric binary relation on var metavariables (irreflexivity is proved by nfnid 5304 with additional axioms; see also nfcv 2901). This could be proved from aecom 2435 and nfcvb 5305 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 2745 instead of equcomd 2026; removing dependency on ax-ext 2711 is possible: prove weak versions (i.e. replace classes with setvars) of drnfc1 2920, eleq2d 2825 (using elequ2 2134), nfcvf 2927, dvelimc 2926, dvelimdc 2925, nfcvf2 2928. (Proof modification is discouraged.)

Assertion

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

Proof of Theorem bj-nfcsym

Step	Hyp	Ref	Expression
1		sp 2195	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)
2	1	equcomd 2026	. . 3 ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑦 = 𝑥)
3	2	drnfc1 2920	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝑦 ↔ Ⅎ𝑦𝑥))
4		nfcvf 2927	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦)
5		nfcvf2 2928	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥)
6	4, 5	2thd 266	. 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝑦 ↔ Ⅎ𝑦𝑥))
7	3, 6	pm2.61i 183	1 ⊢ (Ⅎ𝑥𝑦 ↔ Ⅎ𝑦𝑥)

Syntax hints:  ¬ wn 3   ↔ wb 207  ∀wal 1545  Ⅎwnfc 2886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-13 2380  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791  df-cleq 2731  df-nfc 2888

This theorem is referenced by: (None)