Theorem bj-nfcsym 33457

Description: The nonfreeness quantifier for classes defines a symmetric binary relation on var metavariables (irreflexivity is proved by nfnid 5087 with additional axioms; see also nfcv 2934). This could be proved from aecom 2393 and nfcvb 5088 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 2784 instead of equcomd 2066; removing dependency on ax-ext 2754 is possible: prove weak versions (i.e. replace classes with setvars) of drnfc1 2951, eleq2d 2845 (using elequ2 2121), nfcvf 2960, dvelimc 2959, dvelimdc 2958, nfcvf2 2961. (Proof modification is discouraged.)

Assertion

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

Proof of Theorem bj-nfcsym

Step	Hyp	Ref	Expression
1		sp 2167	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)
2	1	equcomd 2066	. . 3 ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑦 = 𝑥)
3	2	drnfc1 2951	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝑦 ↔ Ⅎ𝑦𝑥))
4		nfcvf 2960	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦)
5		nfcvf2 2961	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥)
6	4, 5	2thd 257	. 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝑦 ↔ Ⅎ𝑦𝑥))
7	3, 6	pm2.61i 177	1 ⊢ (Ⅎ𝑥𝑦 ↔ Ⅎ𝑦𝑥)

Syntax hints:  ¬ wn 3   ↔ wb 198  ∀wal 1599  Ⅎwnfc 2919

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-cleq 2770  df-clel 2774  df-nfc 2921

This theorem is referenced by: (None)