Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-nfcsym Structured version   Visualization version   GIF version

Theorem bj-nfcsym 34821
Description: The nonfreeness quantifier for classes defines a symmetric binary relation on var metavariables (irreflexivity is proved by nfnid 5268 with additional axioms; see also nfcv 2904). This could be proved from aecom 2426 and nfcvb 5269 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 2743 instead of equcomd 2027; removing dependency on ax-ext 2708 is possible: prove weak versions (i.e. replace classes with setvars) of drnfc1 2923, eleq2d 2823 (using elequ2 2125), nfcvf 2933, dvelimc 2932, dvelimdc 2931, nfcvf2 2934. (Proof modification is discouraged.)
Assertion
Ref Expression
bj-nfcsym (𝑥𝑦𝑦𝑥)

Proof of Theorem bj-nfcsym
StepHypRef Expression
1 sp 2180 . . . 4 (∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)
21equcomd 2027 . . 3 (∀𝑥 𝑥 = 𝑦𝑦 = 𝑥)
32drnfc1 2923 . 2 (∀𝑥 𝑥 = 𝑦 → (𝑥𝑦𝑦𝑥))
4 nfcvf 2933 . . 3 (¬ ∀𝑥 𝑥 = 𝑦𝑥𝑦)
5 nfcvf2 2934 . . 3 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑥)
64, 52thd 268 . 2 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥𝑦𝑦𝑥))
73, 6pm2.61i 185 1 (𝑥𝑦𝑦𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 209  wal 1541  wnfc 2884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-13 2371  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-nf 1792  df-cleq 2729  df-nfc 2886
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator