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

Theorem nfi 1623
Description: Deduce that is not free in from the definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfi.1
Assertion
Ref Expression
nfi

Proof of Theorem nfi
StepHypRef Expression
1 df-nf 1617 . 2
2 nfi.1 . 2
31, 2mpgbir 1622 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  A.wal 1393  F/wnf 1616
This theorem is referenced by:  nfth  1625  nfnth  1628  nfv  1707  nfe1  1840  nfdh  1879  19.9h  1891  nfa1  1897  19.21h  1907  19.23h  1911  exlimih  1913  exlimdh  1915  nfdi  1916  nfim1  1919  nfan1  1927  hban  1931  hb3an  1932  nfal  1947  nfex  1948  dvelimhw  1955  nfdiOLD  1963  cbv3h  2016  equsalh  2037  equsexh  2039  nfae  2056  axc16i  2064  dvelimh  2078  nfs1  2104  sbh  2122  nfs1v  2181  hbsb  2185  sb7h  2198  nfequid-o  2240  nfa1-o  2245  nfsab1  2446  nfsab  2448  cleqh  2572  nfcii  2609  nfcri  2612  wl-nfalv  29977  2sb5ndVD  33710  2sb5ndALT  33732  bnj596  33803  bnj1146  33850  bnj1379  33889  bnj1464  33902  bnj1468  33904  bnj605  33965  bnj607  33974  bnj916  33991  bnj964  34001  bnj981  34008  bnj983  34009  bnj1014  34018  bnj1123  34042  bnj1373  34086  bnj1417  34097  bnj1445  34100  bnj1463  34111  bnj1497  34116  bj-cbv3hv  34290  bj-cbv3hv2  34291  bj-equsalhv  34311  bj-equsexhv  34314  bj-nfs1v  34353  bj-nfsab1  34357  bj-nfcri  34428
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618
This theorem depends on definitions:  df-bi 185  df-nf 1617
  Copyright terms: Public domain W3C validator