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

Theorem nfcii 2619
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 1606 . 2  |-  F/ x  y  e.  A
32nfci 2618 1  |-  F/_ x A
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1377    e. wcel 1767   F/_wnfc 2615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601
This theorem depends on definitions:  df-bi 185  df-nf 1600  df-nfc 2617
This theorem is referenced by:  bnj1316  32958  bnj1385  32970  bnj1400  32973  bnj1468  32983  bnj1534  32990  bnj1542  32994  bnj1228  33146  bnj1307  33158  bnj1448  33182  bnj1466  33188  bnj1463  33190  bnj1491  33192  bnj1312  33193  bnj1498  33196  bnj1520  33201  bnj1525  33204  bnj1529  33205  bnj1523  33206
  Copyright terms: Public domain W3C validator