Theorem nfra1 2525

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 2477	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		nfa1 1552	. 2 |- F/ x A. x ( x e. A -> ph )
3	1, 2	nfxfr 1485	1 |- F/ x A. x e. A ph

Syntax hints:   -> wi 4   A.wal 1362   F/wnf 1471   e. wcel 2164   A.wral 2472

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 1458  ax-gen 1460  ax-ial 1545

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477

This theorem is referenced by:  nfra2xy  2536  r19.12  2600  ralbi  2626  rexbi  2627  nfss  3173  ralidm  3548  nfii1  3944  dfiun2g  3945  mpteq12f  4110  reusv1  4490  ralxfrALT  4499  peano2  4628  fun11iun  5522  fvmptssdm  5643  ffnfv  5717  riota5f  5899  mpoeq123  5978  tfri3  6422  nfixp1  6774  nneneq  6915  exmidomni  7203  mkvprop  7219  caucvgsrlemgt1  7857  suplocsrlem  7870  lble  8968  indstr  9661  nninfinf  10517  fimaxre2  11373  prodeq2  11703  zsupcllemstep  12085  bezoutlemmain  12138  bezoutlemzz  12142  exmidunben  12586  mulcncf  14787  limccnp2cntop  14856  bj-rspgt  15348  isomninnlem  15590  iswomninnlem  15609  ismkvnnlem  15612