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

Theorem nfra1 2403
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 2358 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 nfa1 1475 . 2 𝑥𝑥(𝑥𝐴𝜑)
31, 2nfxfr 1404 1 𝑥𝑥𝐴 𝜑
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1283  wnf 1390  wcel 1434  wral 2353
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ial 1468
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-ral 2358
This theorem is referenced by:  nfra2xy  2412  r19.12  2472  ralbi  2495  rexbi  2496  nfss  3003  ralidm  3363  nfii1  3735  dfiun2g  3736  mpteq12f  3884  reusv1  4244  ralxfrALT  4253  peano2  4373  fun11iun  5222  fvmptssdm  5332  ffnfv  5398  riota5f  5571  mpt2eq123  5643  tfri3  6064  nneneq  6503  exmidomni  6703  caucvgsrlemgt1  7243  lble  8302  indstr  8976  fimaxre2  10483  zsupcllemstep  10721  bezoutlemmain  10767  bezoutlemzz  10771  bj-rspgt  11029
  Copyright terms: Public domain W3C validator