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  3172  ralidm  3547  nfii1  3943  dfiun2g  3944  mpteq12f  4109  reusv1  4489  ralxfrALT  4498  peano2  4627  fun11iun  5521  fvmptssdm  5642  ffnfv  5716  riota5f  5898  mpoeq123  5977  tfri3  6420  nfixp1  6772  nneneq  6913  exmidomni  7201  mkvprop  7217  caucvgsrlemgt1  7855  suplocsrlem  7868  lble  8966  indstr  9658  nninfinf  10514  fimaxre2  11370  prodeq2  11700  zsupcllemstep  12082  bezoutlemmain  12135  bezoutlemzz  12139  exmidunben  12583  mulcncf  14762  limccnp2cntop  14831  bj-rspgt  15278  isomninnlem  15520  iswomninnlem  15539  ismkvnnlem  15542