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  5526  fvmptssdm  5647  ffnfv  5721  riota5f  5903  mpoeq123  5983  tfri3  6427  nfixp1  6779  nneneq  6920  exmidomni  7210  mkvprop  7226  caucvgsrlemgt1  7865  suplocsrlem  7878  lble  8977  indstr  9670  zsupcllemstep  10322  nninfinf  10538  fimaxre2  11395  prodeq2  11725  bezoutlemmain  12176  bezoutlemzz  12180  exmidunben  12654  mulcncf  14870  limccnp2cntop  14939  bj-rspgt  15458  isomninnlem  15703  iswomninnlem  15722  ismkvnnlem  15725