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

Theorem nfcii 2887
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 2142 . 2 𝑥 𝑦𝐴
32nfci 2886 1 𝑥𝐴
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1539  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  ax-4 1811  ax-10 2137
This theorem depends on definitions:  df-bi 206  df-ex 1782  df-nf 1786  df-nfc 2885
This theorem is referenced by:  bnj1316  33726  bnj1385  33738  bnj1400  33741  bnj1468  33752  bnj1534  33759  bnj1542  33763  bnj1228  33917  bnj1307  33929  bnj1448  33953  bnj1466  33959  bnj1463  33961  bnj1491  33963  bnj1312  33964  bnj1498  33967  bnj1520  33972  bnj1525  33975  bnj1529  33976  bnj1523  33977
  Copyright terms: Public domain W3C validator