Theorem nfra1 2573

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 2525	. 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 2203   A.wral 2520

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 2525

This theorem is referenced by:  nfra2xy  2584  r19.12  2649  ralbi  2675  rexbi  2676  nfss  3231  ralidm  3610  nfii1  4022  dfiun2g  4023  mpteq12f  4190  reusv1  4579  ralxfrALT  4588  peano2  4717  fun11iun  5635  fvmptssdm  5762  ffnfv  5835  riota5f  6030  mpoeq123  6112  tfri3  6598  nfixp1  6953  nneneq  7111  exmidomni  7433  mkvprop  7449  caucvgsrlemgt1  8110  suplocsrlem  8123  lble  9221  indstr  9925  zsupcllemstep  10589  nninfinf  10805  fimaxre2  11912  prodeq2  12243  bezoutlemmain  12694  bezoutlemzz  12698  exmidunben  13177  mulcncf  15473  limccnp2cntop  15542  bj-rspgt  16558  isomninnlem  16814  iswomninnlem  16834  ismkvnnlem  16837