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  3176  ralidm  3551  nfii1  3947  dfiun2g  3948  mpteq12f  4113  reusv1  4493  ralxfrALT  4502  peano2  4631  fun11iun  5525  fvmptssdm  5646  ffnfv  5720  riota5f  5902  mpoeq123  5981  tfri3  6425  nfixp1  6777  nneneq  6918  exmidomni  7208  mkvprop  7224  caucvgsrlemgt1  7862  suplocsrlem  7875  lble  8974  indstr  9667  zsupcllemstep  10319  nninfinf  10535  fimaxre2  11392  prodeq2  11722  bezoutlemmain  12165  bezoutlemzz  12169  exmidunben  12643  mulcncf  14844  limccnp2cntop  14913  bj-rspgt  15432  isomninnlem  15674  iswomninnlem  15693  ismkvnnlem  15696