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

Theorem nfa1 1897
Description: is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfa1

Proof of Theorem nfa1
StepHypRef Expression
1 hba1 1896 . 2
21nfi 1623 1
Colors of variables: wff setvar class
Syntax hints:  A.wal 1393  F/wnf 1616
This theorem is referenced by:  axc4i  1898  nfnf1  1899  nfna1  1903  ax16nf  1944  19.12  1950  nfa2  1953  nfia1  1954  nf2  1960  equs5a  1978  equs5e  1979  cbv1h  2018  dral1  2067  nfald2  2073  ax12v2  2083  equs5  2092  axc14  2113  sbf2  2123  nfsb4t  2130  sbcom3  2153  sb56  2172  exsb  2212  nfeu1  2294  mo3OLD  2324  moexex  2363  2eu1OLD  2377  2eu4OLD  2381  2eu6  2383  exists2  2389  nfaba1  2624  nfra1  2838  ceqsalgALT  3135  elrab3t  3256  csbie2t  3463  sbcnestgf  3839  dfnfc2  4267  mpteq12f  4528  axrep2  4565  axrep3  4566  axrep4  4567  alxfr  4665  copsex2t  4739  mosubopt  4750  fv3  5884  fvmptt  5971  fnoprabg  6403  pssnn  7758  fiint  7817  aceq1  8519  zorn2lem4  8900  axpowndlem3OLD  8997  zfcndrep  9013  mreexexd  15045  dfon2lem7  29221  wl-nfimf1  29978  wl-nfae1  29980  wl-sb8t  30000  wl-sbnf1  30003  wl-lem-moexsb  30017  wl-mo2t  30020  wl-mo3t  30021  wl-sb8eut  30022  wl-ax11-lem3  30027  wl-sbcom3  30035  sbali  30515  nfbii2  30567  setindtr  30966  axc11next  31313  iotain  31324  pm14.122b  31330  pm14.123b  31333  eubi  31343  rexsb  32173  ax6e2ndeqVD  33709  e2ebindALT  33729  ax6e2ndeqALT  33731  bj-alalbial  34255  bj-exalbial  34256  bj-biexal1  34259  bj-bialal  34262  bj-cbv1hv  34293  bj-ax16nf  34324  bj-dral1v  34326  bj-axc15v  34330  bj-equs5v  34332  bj-sb56  34349  bj-axrep2  34375  bj-axrep3  34376  bj-axrep4  34377  ax11-pm  34405  bj-snsetex  34521
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-12 1854
This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617
  Copyright terms: Public domain W3C validator