MPE Home 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