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

Theorem nfci 2886
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 2885 . 2 (𝑥𝐴 ↔ ∀𝑦𝑥 𝑦𝐴)
2 nfci.1 . 2 𝑥 𝑦𝐴
31, 2mpgbir 1801 1 𝑥𝐴
Colors of variables: wff setvar class
Syntax hints:  wnf 1785  wcel 2106  wnfc 2883
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 206  df-nfc 2885
This theorem is referenced by:  nfcii  2887  nfcv  2903  nfab1  2905  nfab  2909  nfabg  2910  iinabrex  31729  fpwrelmap  31893  esumfzf  32962  fsumiunss  44128  climsuse  44161  climinff  44164  fnlimfvre  44227  limsupre3uzlem  44288  pimdecfgtioc  45268  pimincfltioc  45269  smfmullem4  45347  smflimsupmpt  45382
  Copyright terms: Public domain W3C validator