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

Theorem nfcii 2423
 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
21nfi 1541 . 2
32nfci 2422 1
 Colors of variables: wff set class Syntax hints:   wi 4  wal 1530   wcel 1696  wnfc 2419 This theorem is referenced by:  gsumdixp  15408  bnj1316  29169  bnj1385  29181  bnj1400  29184  bnj1468  29194  bnj1534  29201  bnj1542  29205  bnj1228  29357  bnj1307  29369  bnj1311  29370  bnj1448  29393  bnj1466  29399  bnj1463  29401  bnj1491  29403  bnj1312  29404  bnj1498  29407  bnj1520  29412  bnj1525  29415  bnj1529  29416  bnj1523  29417 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536 This theorem depends on definitions:  df-bi 177  df-nf 1535  df-nfc 2421
 Copyright terms: Public domain W3C validator