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

Theorem nfci 2961
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 2960 . 2 (𝑥𝐴 ↔ ∀𝑦𝑥 𝑦𝐴)
2 nfci.1 . 2 𝑥 𝑦𝐴
31, 2mpgbir 1791 1 𝑥𝐴
Colors of variables: wff setvar class
Syntax hints:  wnf 1775  wcel 2105  wnfc 2958
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787
This theorem depends on definitions:  df-bi 208  df-nfc 2960
This theorem is referenced by:  nfcii  2962  nfcv  2974  nfab1  2976  nfab  2981  nfabg  2982  fpwrelmap  30395  esumfzf  31227  fsumiunss  41732  climsuse  41765  climinff  41768  fnlimfvre  41831  limsupre3uzlem  41892  pimdecfgtioc  42870  pimincfltioc  42871  smfmullem4  42946  smflimsupmpt  42980
  Copyright terms: Public domain W3C validator