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

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

Proof of Theorem nfcii
StepHypRef Expression
1 nfcii.1 . . 3 (𝑦𝐴 → ∀𝑥 𝑦𝐴)
21nf5i 2146 . 2 𝑥 𝑦𝐴
32nfci 2887 1 𝑥𝐴
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1541  wcel 2110  wnfc 2884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-10 2141
This theorem depends on definitions:  df-bi 210  df-ex 1788  df-nf 1792  df-nfc 2886
This theorem is referenced by:  bnj1316  32513  bnj1385  32525  bnj1400  32528  bnj1468  32539  bnj1534  32546  bnj1542  32550  bnj1228  32704  bnj1307  32716  bnj1448  32740  bnj1466  32746  bnj1463  32748  bnj1491  32750  bnj1312  32751  bnj1498  32754  bnj1520  32759  bnj1525  32762  bnj1529  32763  bnj1523  32764
  Copyright terms: Public domain W3C validator