Theorem nfra1 2537

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 2489	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		nfa1 1564	. 2 |- F/ x A. x ( x e. A -> ph )
3	1, 2	nfxfr 1497	1 |- F/ x A. x e. A ph

Syntax hints:   -> wi 4   A.wal 1371   F/wnf 1483   e. wcel 2176   A.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  4125  reusv1  4506  ralxfrALT  4515  peano2  4644  fun11iun  5545  fvmptssdm  5666  ffnfv  5740  riota5f  5926  mpoeq123  6006  tfri3  6455  nfixp1  6807  nneneq  6956  exmidomni  7246  mkvprop  7262  caucvgsrlemgt1  7910  suplocsrlem  7923  lble  9022  indstr  9716  zsupcllemstep  10374  nninfinf  10590  fimaxre2  11571  prodeq2  11901  bezoutlemmain  12352  bezoutlemzz  12356  exmidunben  12830  mulcncf  15113  limccnp2cntop  15182  bj-rspgt  15759  isomninnlem  16006  iswomninnlem  16025  ismkvnnlem  16028