Theorem nfra1 2528

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 2480	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		nfa1 1555	. 2 |- F/ x A. x ( x e. A -> ph )
3	1, 2	nfxfr 1488	1 |- F/ x A. x e. A ph

Syntax hints:   -> wi 4   A.wal 1362   F/wnf 1474   e. wcel 2167   A.wral 2475

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 1461  ax-gen 1463  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480

This theorem is referenced by:  nfra2xy  2539  r19.12  2603  ralbi  2629  rexbi  2630  nfss  3177  ralidm  3552  nfii1  3948  dfiun2g  3949  mpteq12f  4114  reusv1  4494  ralxfrALT  4503  peano2  4632  fun11iun  5528  fvmptssdm  5649  ffnfv  5723  riota5f  5905  mpoeq123  5985  tfri3  6434  nfixp1  6786  nneneq  6927  exmidomni  7217  mkvprop  7233  caucvgsrlemgt1  7879  suplocsrlem  7892  lble  8991  indstr  9684  zsupcllemstep  10336  nninfinf  10552  fimaxre2  11409  prodeq2  11739  bezoutlemmain  12190  bezoutlemzz  12194  exmidunben  12668  mulcncf  14928  limccnp2cntop  14997  bj-rspgt  15516  isomninnlem  15761  iswomninnlem  15780  ismkvnnlem  15783