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

Theorem nfcvf2 2642
Description: If and are distinct, then is not free in . (Contributed by Mario Carneiro, 5-Dec-2016.)
Assertion
Ref Expression
nfcvf2

Proof of Theorem nfcvf2
StepHypRef Expression
1 nfcvf 2641 . 2
21naecoms 2013 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  A.wal 1368  F/_wnfc 2602
This theorem is referenced by:  dfid3  4754  oprabid  6246  axrepndlem1  8893  axrepndlem2  8894  axrepnd  8895  axunnd  8897  axpowndlem2OLD  8900  axpowndlem3  8901  axpowndlem3OLD  8902  axpowndlem4  8903  axpownd  8904  axregndlem2  8906  axinfndlem1  8909  axinfnd  8910  axacndlem4  8914  axacndlem5  8915  axacnd  8916  bj-nfcsym  33240
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-cleq 2446  df-clel 2449  df-nfc 2604
  Copyright terms: Public domain W3C validator