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 36901
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 2431 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 2742 instead of equcomd 2017; removing dependency on ax-ext 2707 is possible: prove weak versions (i.e. replace classes with setvars) of drnfc1 2924, eleq2d 2826 (using elequ2 2122), nfcvf 2931, dvelimc 2930, dvelimdc 2929, nfcvf2 2932. (Proof modification is discouraged.)
Assertion
Ref Expression
bj-nfcsym (𝑥𝑦𝑦𝑥)

Proof of Theorem bj-nfcsym
StepHypRef Expression
1 sp 2182 . . . 4 (∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)
21equcomd 2017 . . 3 (∀𝑥 𝑥 = 𝑦𝑦 = 𝑥)
32drnfc1 2924 . 2 (∀𝑥 𝑥 = 𝑦 → (𝑥𝑦𝑦𝑥))
4 nfcvf 2931 . . 3 (¬ ∀𝑥 𝑥 = 𝑦𝑥𝑦)
5 nfcvf2 2932 . . 3 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑥)
64, 52thd 265 . 2 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥𝑦𝑦𝑥))
73, 6pm2.61i 182 1 (𝑥𝑦𝑦𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wal 1537  wnfc 2889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-13 2376  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-nf 1783  df-cleq 2728  df-nfc 2891
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator