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

Theorem nfcii 2754
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 2023 . 2 𝑥 𝑦𝐴
32nfci 2753 1 𝑥𝐴
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1480  wcel 1989  wnfc 2750
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-10 2018
This theorem depends on definitions:  df-bi 197  df-ex 1704  df-nf 1709  df-nfc 2752
This theorem is referenced by:  bnj1316  30876  bnj1385  30888  bnj1400  30891  bnj1468  30901  bnj1534  30908  bnj1542  30912  bnj1228  31064  bnj1307  31076  bnj1448  31100  bnj1466  31106  bnj1463  31108  bnj1491  31110  bnj1312  31111  bnj1498  31114  bnj1520  31119  bnj1525  31122  bnj1529  31123  bnj1523  31124
  Copyright terms: Public domain W3C validator