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

Theorem bj-nfcsym 33758
Description: The class-form not-free predicate defines a symmetric binary relation on var metavariables (irreflexivity is proved by nfnid 4676 with additional axioms; see also nfcv 2629). This could be proved from aecom 2024 and nfcvb 4677 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 2475 instead of bj-equcomd 33535; removing dependency on ax-ext 2445 is possible: prove weak versions (i.e. replace classes with setvars) of drnfc1 2648, eleq2d 2537 (using elequ2 1772), nfcvf 2654, dvelimc 2653, dvelimdc 2652, nfcvf2 2655. (Proof modification is discouraged.)
Assertion
Ref Expression
bj-nfcsym  |-  ( F/_ x y  <->  F/_ y x )

Proof of Theorem bj-nfcsym
StepHypRef Expression
1 sp 1808 . . . 4  |-  ( A. x  x  =  y  ->  x  =  y )
21bj-equcomd 33535 . . 3  |-  ( A. x  x  =  y  ->  y  =  x )
32drnfc1 2648 . 2  |-  ( A. x  x  =  y  ->  ( F/_ x y  <->  F/_ y x ) )
4 nfcvf 2654 . . 3  |-  ( -. 
A. x  x  =  y  ->  F/_ x y )
5 nfcvf2 2655 . . 3  |-  ( -. 
A. x  x  =  y  ->  F/_ y x )
64, 52thd 240 . 2  |-  ( -. 
A. x  x  =  y  ->  ( F/_ x y  <->  F/_ y x ) )
73, 6pm2.61i 164 1  |-  ( F/_ x y  <->  F/_ y x )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184   A.wal 1377   F/_wnfc 2615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-cleq 2459  df-clel 2462  df-nfc 2617
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator