Theorem nfra1 2581

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

Syntax hints:   → wi 4  ∀wal 1400  Ⅎwnf 1513   ∈ wcel 2209  ∀wral 2528

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 1500  ax-gen 1502  ax-ial 1587

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is referenced by:  nfra2xy  2592  r19.12  2657  ralbi  2683  rexbi  2684  nfss  3241  ralidm  3625  nfii1  4038  dfiun2g  4039  mpteq12f  4206  reusv1  4599  ralxfrALT  4608  peano2  4737  fun11iun  5655  fvmptssdm  5784  ffnfv  5857  riota5f  6055  mpoeq123  6137  abrexss  6348  tfri3  6628  nfixp1  6990  nneneq  7148  exmidomni  7472  mkvprop  7488  caucvgsrlemgt1  8152  suplocsrlem  8165  lble  9267  indstr  9972  zsupcllemstep  10640  nninfinf  10858  fimaxre2  11971  prodeq2  12302  bezoutlemmain  12753  bezoutlemzz  12757  exmidunben  13295  mulcncf  15632  limccnp2cntop  15701  bj-rspgt  16728  isomninnlem  16984  iswomninnlem  17004  ismkvnnlem  17007