Theorem nfra1 2355

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 2311	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		nfa1 1434	. 2 |- F/ x A. x ( x e. A -> ph )
3	1, 2	nfxfr 1363	1 |- F/ x A. x e. A ph

Syntax hints:   -> wi 4   A.wal 1241   F/wnf 1349   e. wcel 1393   A.wral 2306

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ial 1427

This theorem depends on definitions:  df-bi 110  df-nf 1350  df-ral 2311

This theorem is referenced by:  nfra2xy  2364  r19.12  2422  ralbi  2445  rexbi  2446  nfss  2938  ralidm  3321  nfii1  3688  dfiun2g  3689  mpteq12f  3837  reusv1  4190  ralxfrALT  4199  peano2  4318  fun11iun  5147  fvmptssdm  5255  ffnfv  5323  riota5f  5492  mpt2eq123  5564  tfri3  5953  nneneq  6320  caucvgsrlemgt1  6879  indstr  8536  bj-rspgt  9925