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

Theorem nfex 1599
Description: If  x is not free in  ph, it is not free in  E. y ph. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
Hypothesis
Ref Expression
nfex.1  |-  F/ x ph
Assertion
Ref Expression
nfex  |-  F/ x E. y ph

Proof of Theorem nfex
StepHypRef Expression
1 nfex.1 . . . 4  |-  F/ x ph
21nfri 1482 . . 3  |-  ( ph  ->  A. x ph )
32hbex 1598 . 2  |-  ( E. y ph  ->  A. x E. y ph )
43nfi 1421 1  |-  F/ x E. y ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1419   E.wex 1451
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470
This theorem depends on definitions:  df-bi 116  df-nf 1420
This theorem is referenced by:  eeor  1656  cbvex2  1872  eean  1881  nfeu1  1986  nfeuv  1993  nfel  2265  ceqsex2  2698  nfopab  3964  nfopab2  3966  cbvopab1  3969  cbvopab1s  3971  repizf2  4054  copsex2t  4135  copsex2g  4136  euotd  4144  onintrab2im  4402  mosubopt  4572  nfco  4672  dfdmf  4700  dfrnf  4748  nfdm  4751  fv3  5410  nfoprab2  5787  nfoprab3  5788  nfoprab  5789  cbvoprab1  5809  cbvoprab2  5810  cbvoprab3  5813  cnvoprab  6097  ac6sfi  6758  nfsum1  11076  nfsum  11077  fsum2dlemstep  11154
  Copyright terms: Public domain W3C validator