Theorem nfra1 2508

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 2460	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		nfa1 1541	. 2 ⊢ Ⅎ𝑥∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
3	1, 2	nfxfr 1474	1 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝜑

Syntax hints:   → wi 4  ∀wal 1351  Ⅎwnf 1460   ∈ wcel 2148  ∀wral 2455

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 1447  ax-gen 1449  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460

This theorem is referenced by:  nfra2xy  2519  r19.12  2583  ralbi  2609  rexbi  2610  nfss  3148  ralidm  3523  nfii1  3917  dfiun2g  3918  mpteq12f  4083  reusv1  4458  ralxfrALT  4467  peano2  4594  fun11iun  5482  fvmptssdm  5600  ffnfv  5674  riota5f  5854  mpoeq123  5933  tfri3  6367  nfixp1  6717  nneneq  6856  exmidomni  7139  mkvprop  7155  caucvgsrlemgt1  7793  suplocsrlem  7806  lble  8903  indstr  9592  fimaxre2  11234  prodeq2  11564  zsupcllemstep  11945  bezoutlemmain  11998  bezoutlemzz  12002  exmidunben  12426  mulcncf  14061  limccnp2cntop  14116  bj-rspgt  14508  isomninnlem  14748  iswomninnlem  14767  ismkvnnlem  14770