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

Theorem nfex 1637
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 1519 . . 3  |-  ( ph  ->  A. x ph )
32hbex 1636 . 2  |-  ( E. y ph  ->  A. x E. y ph )
43nfi 1462 1  |-  F/ x E. y ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1460   E.wex 1492
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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510
This theorem depends on definitions:  df-bi 117  df-nf 1461
This theorem is referenced by:  eeor  1695  cbvexv1  1752  cbvex2  1922  eean  1931  nfsbv  1947  nfeu1  2037  nfeuv  2044  nfel  2328  ceqsex2  2777  nfopab  4070  nfopab2  4072  cbvopab1  4075  cbvopab1s  4077  repizf2  4161  copsex2t  4244  copsex2g  4245  euotd  4253  onintrab2im  4516  mosubopt  4690  nfco  4791  dfdmf  4819  dfrnf  4867  nfdm  4870  fv3  5537  nfoprab2  5922  nfoprab3  5923  nfoprab  5924  cbvoprab1  5944  cbvoprab2  5945  cbvoprab3  5948  cnvoprab  6232  ac6sfi  6895  cc3  7264  nfsum1  11357  nfsum  11358  fsum2dlemstep  11435  nfcprod1  11555  nfcprod  11556  fprod2dlemstep  11623
  Copyright terms: Public domain W3C validator