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

Theorem nfcii 2568
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 1596 . 2  |-  F/ x  y  e.  A
32nfci 2567 1  |-  F/_ x A
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1367    e. wcel 1756   F/_wnfc 2564
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591
This theorem depends on definitions:  df-bi 185  df-nf 1590  df-nfc 2566
This theorem is referenced by:  bnj1316  31811  bnj1385  31823  bnj1400  31826  bnj1468  31836  bnj1534  31843  bnj1542  31847  bnj1228  31999  bnj1307  32011  bnj1448  32035  bnj1466  32041  bnj1463  32043  bnj1491  32045  bnj1312  32046  bnj1498  32049  bnj1520  32054  bnj1525  32057  bnj1529  32058  bnj1523  32059
  Copyright terms: Public domain W3C validator