Theorem nfra1 2501

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 2453	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		nfa1 1534	. 2 |- F/ x A. x ( x e. A -> ph )
3	1, 2	nfxfr 1467	1 |- F/ x A. x e. A ph

Syntax hints:   -> wi 4   A.wal 1346   F/wnf 1453   e. wcel 2141   A.wral 2448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ial 1527

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453

This theorem is referenced by:  nfra2xy  2512  r19.12  2576  ralbi  2602  rexbi  2603  nfss  3140  ralidm  3515  nfii1  3904  dfiun2g  3905  mpteq12f  4069  reusv1  4443  ralxfrALT  4452  peano2  4579  fun11iun  5463  fvmptssdm  5580  ffnfv  5654  riota5f  5833  mpoeq123  5912  tfri3  6346  nfixp1  6696  nneneq  6835  exmidomni  7118  mkvprop  7134  caucvgsrlemgt1  7757  suplocsrlem  7770  lble  8863  indstr  9552  fimaxre2  11190  prodeq2  11520  zsupcllemstep  11900  bezoutlemmain  11953  bezoutlemzz  11957  exmidunben  12381  mulcncf  13385  limccnp2cntop  13440  bj-rspgt  13821  isomninnlem  14062  iswomninnlem  14081  ismkvnnlem  14084