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

Theorem nfcii 2563
Description: Deduce that a class  A does not have  x free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfcii.1  |-  ( y  e.  A  ->  A. x  y  e.  A )
Assertion
Ref Expression
nfcii  |-  F/_ x A
Distinct variable groups:    x, y    y, A
Allowed substitution hint:    A( x)

Proof of Theorem nfcii
StepHypRef Expression
1 nfcii.1 . . 3  |-  ( y  e.  A  ->  A. x  y  e.  A )
21nfi 1560 . 2  |-  F/ x  y  e.  A
32nfci 2562 1  |-  F/_ x A
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1549    e. wcel 1725   F/_wnfc 2559
This theorem is referenced by:  bnj1316  29192  bnj1385  29204  bnj1400  29207  bnj1468  29217  bnj1534  29224  bnj1542  29228  bnj1228  29380  bnj1307  29392  bnj1448  29416  bnj1466  29422  bnj1463  29424  bnj1491  29426  bnj1312  29427  bnj1498  29430  bnj1520  29435  bnj1525  29438  bnj1529  29439  bnj1523  29440
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555
This theorem depends on definitions:  df-bi 178  df-nf 1554  df-nfc 2561
  Copyright terms: Public domain W3C validator