Theorem nfra1 2537

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

Syntax hints:   → wi 4  ∀wal 1371  Ⅎwnf 1483   ∈ wcel 2176  ∀wral 2484

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 1470  ax-gen 1472  ax-ial 1557

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489

This theorem is referenced by:  nfra2xy  2548  r19.12  2612  ralbi  2638  rexbi  2639  nfss  3186  ralidm  3561  nfii1  3958  dfiun2g  3959  mpteq12f  4124  reusv1  4505  ralxfrALT  4514  peano2  4643  fun11iun  5543  fvmptssdm  5664  ffnfv  5738  riota5f  5924  mpoeq123  6004  tfri3  6453  nfixp1  6805  nneneq  6954  exmidomni  7244  mkvprop  7260  caucvgsrlemgt1  7908  suplocsrlem  7921  lble  9020  indstr  9714  zsupcllemstep  10372  nninfinf  10588  fimaxre2  11538  prodeq2  11868  bezoutlemmain  12319  bezoutlemzz  12323  exmidunben  12797  mulcncf  15080  limccnp2cntop  15149  bj-rspgt  15722  isomninnlem  15969  iswomninnlem  15988  ismkvnnlem  15991