Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfra1 Unicode version

Theorem nfra1 2488
 Description: is not free in . (Contributed by NM, 18-Oct-1996.) (Revised by Mario Carneiro, 7-Oct-2016.)
Assertion
Ref Expression
nfra1

Proof of Theorem nfra1
StepHypRef Expression
1 df-ral 2440 . 2
2 nfa1 1521 . 2
31, 2nfxfr 1454 1
 Colors of variables: wff set class Syntax hints:   wi 4  wal 1333  wnf 1440   wcel 2128  wral 2435 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-ial 1514 This theorem depends on definitions:  df-bi 116  df-nf 1441  df-ral 2440 This theorem is referenced by:  nfra2xy  2499  r19.12  2563  ralbi  2589  rexbi  2590  nfss  3121  ralidm  3494  nfii1  3880  dfiun2g  3881  mpteq12f  4044  reusv1  4416  ralxfrALT  4425  peano2  4552  fun11iun  5432  fvmptssdm  5549  ffnfv  5622  riota5f  5798  mpoeq123  5874  tfri3  6308  nfixp1  6656  nneneq  6795  exmidomni  7068  mkvprop  7084  caucvgsrlemgt1  7698  suplocsrlem  7711  lble  8801  indstr  9487  fimaxre2  11108  prodeq2  11436  zsupcllemstep  11813  bezoutlemmain  11862  bezoutlemzz  11866  exmidunben  12127  mulcncf  12951  limccnp2cntop  13006  bj-rspgt  13319  isomninnlem  13563  iswomninnlem  13582  ismkvnnlem  13585
 Copyright terms: Public domain W3C validator