Theorem nfra1 2564

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 2516	. 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 2202   A.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  7401  mkvprop  7417  caucvgsrlemgt1  8075  suplocsrlem  8088  lble  9186  indstr  9888  zsupcllemstep  10552  nninfinf  10768  fimaxre2  11867  prodeq2  12198  bezoutlemmain  12649  bezoutlemzz  12653  exmidunben  13127  mulcncf  15419  limccnp2cntop  15488  bj-rspgt  16504  isomninnlem  16762  iswomninnlem  16782  ismkvnnlem  16785