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

Theorem nfex 1948
 Description: If is not free in , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
Hypothesis
Ref Expression
nfal.1
Assertion
Ref Expression
nfex

Proof of Theorem nfex
StepHypRef Expression
1 nfal.1 . . . 4
21nfri 1874 . . 3
32hbex 1946 . 2
43nfi 1623 1
 Colors of variables: wff setvar class Syntax hints:  E.wex 1612  F/wnf 1616 This theorem is referenced by:  19.12  1950  eeor  1976  eean  1987  eeeanv  1989  cbvex2OLD  2029  nfeu1  2294  moexex  2363  nfelOLD  2633  ceqsex2  3147  nfopab  4517  nfopab2  4519  cbvopab1  4522  cbvopab1s  4524  axrep2  4565  axrep3  4566  axrep4  4567  copsex2t  4739  copsex2g  4740  mosubopt  4750  euotd  4753  nfco  5173  dfdmf  5201  dfrnf  5246  nfdm  5249  fv3  5884  oprabv  6345  nfoprab2  6347  nfoprab3  6348  nfoprab  6349  cbvoprab1  6369  cbvoprab2  6370  cbvoprab3  6373  ac6sfi  7784  aceq1  8519  zfcndrep  9013  zfcndinf  9017  nfsum1  13512  nfsum  13513  fsum2dlem  13585  nfcprod1  13717  nfcprod  13718  fprod2dlem  13784  cnvoprab  27546  nfwrecs  29338  pm11.71  31303  upbdrech  31505  stoweidlem57  31839  bnj981  34008  bnj1388  34089  bnj1445  34100  bnj1489  34112  bj-axrep2  34375  bj-axrep3  34376  bj-axrep4  34377 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854 This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617
 Copyright terms: Public domain W3C validator