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  3149  ralidm  3524  nfii1  3918  dfiun2g  3919  mpteq12f  4084  reusv1  4459  ralxfrALT  4468  peano2  4595  fun11iun  5483  fvmptssdm  5601  ffnfv  5675  riota5f  5855  mpoeq123  5934  tfri3  6368  nfixp1  6718  nneneq  6857  exmidomni  7140  mkvprop  7156  caucvgsrlemgt1  7794  suplocsrlem  7807  lble  8904  indstr  9593  fimaxre2  11235  prodeq2  11565  zsupcllemstep  11946  bezoutlemmain  11999  bezoutlemzz  12003  exmidunben  12427  mulcncf  14094  limccnp2cntop  14149  bj-rspgt  14541  isomninnlem  14781  iswomninnlem  14800  ismkvnnlem  14803