Theorem nfra1 2397

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

Step	Hyp	Ref	Expression
1		df-ral 2353	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		nfa1 1474	. 2 ⊢ Ⅎ𝑥∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
3	1, 2	nfxfr 1403	1 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝜑

Syntax hints:   → wi 4  ∀wal 1282  Ⅎwnf 1389   ∈ wcel 1433  ∀wral 2348

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 1376  ax-gen 1378  ax-ial 1467

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-ral 2353

This theorem is referenced by:  nfra2xy  2406  r19.12  2466  ralbi  2489  rexbi  2490  nfss  2992  ralidm  3341  nfii1  3709  dfiun2g  3710  mpteq12f  3858  reusv1  4208  ralxfrALT  4217  peano2  4336  fun11iun  5167  fvmptssdm  5276  ffnfv  5344  riota5f  5512  mpt2eq123  5584  tfri3  5976  nneneq  6343  caucvgsrlemgt1  6971  lble  8025  indstr  8681  fimaxre2  10109  zsupcllemstep  10341  bezoutlemmain  10387  bezoutlemzz  10391  bj-rspgt  10596