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

Theorem nfcii 2893
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 2145 . 2 𝑥 𝑦𝐴
32nfci 2892 1 𝑥𝐴
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1537  wcel 2107  wnfc 2889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-10 2140
This theorem depends on definitions:  df-bi 207  df-ex 1779  df-nf 1783  df-nfc 2891
This theorem is referenced by:  bnj1316  34835  bnj1385  34847  bnj1400  34850  bnj1468  34861  bnj1534  34868  bnj1542  34872  bnj1228  35026  bnj1307  35038  bnj1448  35062  bnj1466  35068  bnj1463  35070  bnj1491  35072  bnj1312  35073  bnj1498  35076  bnj1520  35081  bnj1525  35084  bnj1529  35085  bnj1523  35086
  Copyright terms: Public domain W3C validator