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  3515  nfii1  3904  dfiun2g  3905  mpteq12f  4069  reusv1  4443  ralxfrALT  4452  peano2  4579  fun11iun  5463  fvmptssdm  5580  ffnfv  5654  riota5f  5833  mpoeq123  5912  tfri3  6346  nfixp1  6696  nneneq  6835  exmidomni  7118  mkvprop  7134  caucvgsrlemgt1  7757  suplocsrlem  7770  lble  8863  indstr  9552  fimaxre2  11190  prodeq2  11520  zsupcllemstep  11900  bezoutlemmain  11953  bezoutlemzz  11957  exmidunben  12381  mulcncf  13385  limccnp2cntop  13440  bj-rspgt  13821  isomninnlem  14062  iswomninnlem  14081  ismkvnnlem  14084
  Copyright terms: Public domain W3C validator