Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfci Structured version   Visualization version   GIF version

Theorem nfci 2942
 Description: Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfci.1 𝑥 𝑦𝐴
Assertion
Ref Expression
nfci 𝑥𝐴
Distinct variable groups:   𝑥,𝑦   𝑦,𝐴
Allowed substitution hint:   𝐴(𝑥)

Proof of Theorem nfci
StepHypRef Expression
1 df-nfc 2941 . 2 (𝑥𝐴 ↔ ∀𝑦𝑥 𝑦𝐴)
2 nfci.1 . 2 𝑥 𝑦𝐴
31, 2mpgbir 1801 1 𝑥𝐴
 Colors of variables: wff setvar class Syntax hints:  Ⅎwnf 1785   ∈ wcel 2112  Ⅎwnfc 2939 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797 This theorem depends on definitions:  df-bi 210  df-nfc 2941 This theorem is referenced by:  nfcii  2943  nfcv  2958  nfab1  2960  nfab  2964  nfabg  2965  iinabrex  30336  fpwrelmap  30499  esumfzf  31442  fsumiunss  42214  climsuse  42247  climinff  42250  fnlimfvre  42313  limsupre3uzlem  42374  pimdecfgtioc  43347  pimincfltioc  43348  smfmullem4  43423  smflimsupmpt  43457
 Copyright terms: Public domain W3C validator