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

Theorem nfra1 2352
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 2308 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 nfa1 1434 . 2 𝑥𝑥(𝑥𝐴𝜑)
31, 2nfxfr 1363 1 𝑥𝑥𝐴 𝜑
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1241  wnf 1349  wcel 1393  wral 2303
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ial 1427
This theorem depends on definitions:  df-bi 110  df-nf 1350  df-ral 2308
This theorem is referenced by:  nfra2xy  2361  r19.12  2419  ralbi  2442  rexbi  2443  nfss  2935  ralidm  3318  nfii1  3685  dfiun2g  3686  mpteq12f  3834  reusv1  4162  ralxfrALT  4171  peano2  4281  fun11iun  5110  fvmptssdm  5218  ffnfv  5286  riota5f  5455  mpt2eq123  5527  tfri3  5916  nneneq  6283  caucvgsrlemgt1  6836  indstr  8484  bj-rspgt  9774
  Copyright terms: Public domain W3C validator