Theorem nfra1 2469

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 2422	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		nfa1 1522	. 2 |- F/ x A. x ( x e. A -> ph )
3	1, 2	nfxfr 1451	1 |- F/ x A. x e. A ph

Syntax hints:   -> wi 4   A.wal 1330   F/wnf 1437   e. wcel 1481   A.wral 2417

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 1424  ax-gen 1426  ax-ial 1515

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422

This theorem is referenced by:  nfra2xy  2478  r19.12  2541  ralbi  2567  rexbi  2568  nfss  3095  ralidm  3468  nfii1  3852  dfiun2g  3853  mpteq12f  4016  reusv1  4387  ralxfrALT  4396  peano2  4517  fun11iun  5396  fvmptssdm  5513  ffnfv  5586  riota5f  5762  mpoeq123  5838  tfri3  6272  nfixp1  6620  nneneq  6759  exmidomni  7022  mkvprop  7040  caucvgsrlemgt1  7627  suplocsrlem  7640  lble  8729  indstr  9415  fimaxre2  11030  prodeq2  11358  zsupcllemstep  11674  bezoutlemmain  11722  bezoutlemzz  11726  exmidunben  11975  mulcncf  12799  limccnp2cntop  12854  bj-rspgt  13164  isomninnlem  13400  iswomninnlem  13417  ismkvnnlem  13419