Theorem nfra1 2575

Description: x is not free in A. x e. A ph. (Contributed by NM, 18-Oct-1996.) (Revised by Mario Carneiro, 7-Oct-2016.)

Assertion

Ref	Expression
nfra1	|- F/ x A. x e. A ph

Proof of Theorem nfra1

Step	Hyp	Ref	Expression
1		df-ral 2527	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		nfa1 1590	. 2 |- F/ x A. x ( x e. A -> ph )
3	1, 2	nfxfr 1523	1 |- F/ x A. x e. A ph

Syntax hints:   -> wi 4   A.wal 1396   F/wnf 1509   e. wcel 2205   A.wral 2522

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 2527

This theorem is referenced by:  nfra2xy  2586  r19.12  2651  ralbi  2677  rexbi  2678  nfss  3235  ralidm  3614  nfii1  4027  dfiun2g  4028  mpteq12f  4195  reusv1  4584  ralxfrALT  4593  peano2  4722  fun11iun  5640  fvmptssdm  5767  ffnfv  5840  riota5f  6038  mpoeq123  6120  abrexss  6331  tfri3  6611  nfixp1  6966  nneneq  7124  exmidomni  7446  mkvprop  7462  caucvgsrlemgt1  8126  suplocsrlem  8139  lble  9238  indstr  9943  zsupcllemstep  10611  nninfinf  10829  fimaxre2  11937  prodeq2  12268  bezoutlemmain  12719  bezoutlemzz  12723  exmidunben  13261  mulcncf  15599  limccnp2cntop  15668  bj-rspgt  16684  isomninnlem  16940  iswomninnlem  16960  ismkvnnlem  16963