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

Theorem nfra1 2443
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 2398 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 nfa1 1506 . 2 𝑥𝑥(𝑥𝐴𝜑)
31, 2nfxfr 1435 1 𝑥𝑥𝐴 𝜑
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1314  wnf 1421  wcel 1465  wral 2393
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 1408  ax-gen 1410  ax-ial 1499
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-ral 2398
This theorem is referenced by:  nfra2xy  2452  r19.12  2515  ralbi  2541  rexbi  2542  nfss  3060  ralidm  3433  nfii1  3814  dfiun2g  3815  mpteq12f  3978  reusv1  4349  ralxfrALT  4358  peano2  4479  fun11iun  5356  fvmptssdm  5473  ffnfv  5546  riota5f  5722  mpoeq123  5798  tfri3  6232  nfixp1  6580  nneneq  6719  exmidomni  6982  mkvprop  7000  caucvgsrlemgt1  7571  suplocsrlem  7584  lble  8673  indstr  9356  fimaxre2  10966  zsupcllemstep  11565  bezoutlemmain  11613  bezoutlemzz  11617  exmidunben  11866  mulcncf  12687  limccnp2cntop  12742  bj-rspgt  12920  isomninnlem  13152
  Copyright terms: Public domain W3C validator