Theorem nfra1 2564

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

Syntax hints:   → wi 4  ∀wal 1396  Ⅎwnf 1509   ∈ wcel 2202  ∀wral 2511

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 1496  ax-gen 1498  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2516

This theorem is referenced by:  nfra2xy  2575  r19.12  2640  ralbi  2666  rexbi  2667  nfss  3221  ralidm  3597  nfii1  4006  dfiun2g  4007  mpteq12f  4174  reusv1  4561  ralxfrALT  4570  peano2  4699  fun11iun  5613  fvmptssdm  5740  ffnfv  5813  riota5f  6008  mpoeq123  6090  tfri3  6576  nfixp1  6930  nneneq  7086  exmidomni  7384  mkvprop  7400  caucvgsrlemgt1  8058  suplocsrlem  8071  lble  9169  indstr  9871  zsupcllemstep  10535  nninfinf  10751  fimaxre2  11850  prodeq2  12181  bezoutlemmain  12632  bezoutlemzz  12636  exmidunben  13110  mulcncf  15402  limccnp2cntop  15471  bj-rspgt  16487  isomninnlem  16745  iswomninnlem  16765  ismkvnnlem  16768