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

Theorem nfcii 2946
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 2191 . 2 𝑥 𝑦𝐴
32nfci 2945 1 𝑥𝐴
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1635  wcel 2157  wnfc 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-10 2186
This theorem depends on definitions:  df-bi 198  df-ex 1860  df-nf 1864  df-nfc 2944
This theorem is referenced by:  bnj1316  31219  bnj1385  31231  bnj1400  31234  bnj1468  31244  bnj1534  31251  bnj1542  31255  bnj1228  31407  bnj1307  31419  bnj1448  31443  bnj1466  31449  bnj1463  31451  bnj1491  31453  bnj1312  31454  bnj1498  31457  bnj1520  31462  bnj1525  31465  bnj1529  31466  bnj1523  31467
  Copyright terms: Public domain W3C validator