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

Theorem nfra1 2501
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 2453 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 nfa1 1534 . 2 𝑥𝑥(𝑥𝐴𝜑)
31, 2nfxfr 1467 1 𝑥𝑥𝐴 𝜑
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1346  wnf 1453  wcel 2141  wral 2448
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 1440  ax-gen 1442  ax-ial 1527
This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453
This theorem is referenced by:  nfra2xy  2512  r19.12  2576  ralbi  2602  rexbi  2603  nfss  3140  ralidm  3514  nfii1  3902  dfiun2g  3903  mpteq12f  4067  reusv1  4441  ralxfrALT  4450  peano2  4577  fun11iun  5461  fvmptssdm  5578  ffnfv  5651  riota5f  5830  mpoeq123  5909  tfri3  6343  nfixp1  6692  nneneq  6831  exmidomni  7114  mkvprop  7130  caucvgsrlemgt1  7744  suplocsrlem  7757  lble  8850  indstr  9539  fimaxre2  11177  prodeq2  11507  zsupcllemstep  11887  bezoutlemmain  11940  bezoutlemzz  11944  exmidunben  12368  mulcncf  13344  limccnp2cntop  13399  bj-rspgt  13780  isomninnlem  14022  iswomninnlem  14041  ismkvnnlem  14044
  Copyright terms: Public domain W3C validator