NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  nfcvd Unicode version

Theorem nfcvd 2490
Description: If is disjoint from , then is not free in . (Contributed by Mario Carneiro, 7-Oct-2016.)
Assertion
Ref Expression
nfcvd  F/_
Distinct variable group:   ,
Allowed substitution hint:   ()

Proof of Theorem nfcvd
StepHypRef Expression
1 nfcv 2489 . 2  F/_
21a1i 10 1  F/_
Colors of variables: wff setvar class
Syntax hints:   wi 4   F/_wnfc 2476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-17 1616
This theorem depends on definitions:  df-bi 177  df-nf 1545  df-nfc 2478
This theorem is referenced by:  nfeld  2504  ralcom2  2775  vtoclgft  2905  vtocld  2907  sbcralt  3118  sbcrext  3119  csbied  3178  csbie2t  3180  sbcco3g  3191  csbco3g  3193  dfnfc2  3909  nfiotad  4342  iota2d  4366  iota2  4367  dfid3  4768  oprabid  5550
  Copyright terms: Public domain W3C validator