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 31244
Description: The class-form not-free predicate defines a symmetric binary relation on var metavariables (irreflexivity is proved by nfnid 4651 with additional axioms; see also nfcv 2591). This could be proved from aecom 2107 and nfcvb 4652 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 2437 instead of bj-equcomd 31014; removing dependency on ax-ext 2407 is possible: prove weak versions (i.e. replace classes with setvars) of drnfc1 2610, eleq2d 2499 (using elequ2 1875), nfcvf 2616, dvelimc 2615, dvelimdc 2614, nfcvf2 2617. (Proof modification is discouraged.)
Assertion
Ref Expression
bj-nfcsym  |-  ( F/_ x y  <->  F/_ y x )

Proof of Theorem bj-nfcsym
StepHypRef Expression
1 sp 1912 . . . 4  |-  ( A. x  x  =  y  ->  x  =  y )
21bj-equcomd 31014 . . 3  |-  ( A. x  x  =  y  ->  y  =  x )
32drnfc1 2610 . 2  |-  ( A. x  x  =  y  ->  ( F/_ x y  <->  F/_ y x ) )
4 nfcvf 2616 . . 3  |-  ( -. 
A. x  x  =  y  ->  F/_ x y )
5 nfcvf2 2617 . . 3  |-  ( -. 
A. x  x  =  y  ->  F/_ y x )
64, 52thd 243 . 2  |-  ( -. 
A. x  x  =  y  ->  ( F/_ x y  <->  F/_ y x ) )
73, 6pm2.61i 167 1  |-  ( F/_ x y  <->  F/_ y x )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 187   A.wal 1435   F/_wnfc 2577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-cleq 2421  df-clel 2424  df-nfc 2579
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator