ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfre1 Unicode version

Theorem nfre1 2415
Description:  x is not free in  E. x  e.  A ph. (Contributed by NM, 19-Mar-1997.) (Revised by Mario Carneiro, 7-Oct-2016.)
Assertion
Ref Expression
nfre1  |-  F/ x E. x  e.  A  ph

Proof of Theorem nfre1
StepHypRef Expression
1 df-rex 2361 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
2 nfe1 1428 . 2  |-  F/ x E. x ( x  e.  A  /\  ph )
31, 2nfxfr 1406 1  |-  F/ x E. x  e.  A  ph
Colors of variables: wff set class
Syntax hints:    /\ wa 102   F/wnf 1392   E.wex 1424    e. wcel 1436   E.wrex 2356
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ie1 1425
This theorem depends on definitions:  df-bi 115  df-nf 1393  df-rex 2361
This theorem is referenced by:  r19.29an  2506  nfiu1  3745  fun11iun  5239  eusvobj2  5601  fodjuomnilemdc  6746  prarloclem3step  7002  prmuloc2  7073  ltexprlemm  7106  caucvgprprlemaddq  7214  caucvgsrlemgt1  7287  supinfneg  9018  infsupneg  9019  lbzbi  9036  divalglemeunn  10846  divalglemeuneg  10848  bezoutlemmain  10912  bezout  10925
  Copyright terms: Public domain W3C validator