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

Theorem nfra1 2518
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 2470 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 nfa1 1551 . 2 𝑥𝑥(𝑥𝐴𝜑)
31, 2nfxfr 1484 1 𝑥𝑥𝐴 𝜑
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1361  wnf 1470  wcel 2158  wral 2465
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1457  ax-gen 1459  ax-ial 1544
This theorem depends on definitions:  df-bi 117  df-nf 1471  df-ral 2470
This theorem is referenced by:  nfra2xy  2529  r19.12  2593  ralbi  2619  rexbi  2620  nfss  3160  ralidm  3535  nfii1  3929  dfiun2g  3930  mpteq12f  4095  reusv1  4470  ralxfrALT  4479  peano2  4606  fun11iun  5494  fvmptssdm  5613  ffnfv  5687  riota5f  5868  mpoeq123  5947  tfri3  6382  nfixp1  6732  nneneq  6871  exmidomni  7154  mkvprop  7170  caucvgsrlemgt1  7808  suplocsrlem  7821  lble  8918  indstr  9607  fimaxre2  11249  prodeq2  11579  zsupcllemstep  11960  bezoutlemmain  12013  bezoutlemzz  12017  exmidunben  12441  mulcncf  14444  limccnp2cntop  14499  bj-rspgt  14891  isomninnlem  15132  iswomninnlem  15151  ismkvnnlem  15154
  Copyright terms: Public domain W3C validator