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

Theorem nfex 1617
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 1499 . . 3  |-  ( ph  ->  A. x ph )
32hbex 1616 . 2  |-  ( E. y ph  ->  A. x E. y ph )
43nfi 1442 1  |-  F/ x E. y ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1440   E.wex 1472
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 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490
This theorem depends on definitions:  df-bi 116  df-nf 1441
This theorem is referenced by:  eeor  1675  cbvexv1  1732  cbvex2  1902  eean  1911  nfsbv  1927  nfeu1  2017  nfeuv  2024  nfel  2308  ceqsex2  2752  nfopab  4034  nfopab2  4036  cbvopab1  4039  cbvopab1s  4041  repizf2  4125  copsex2t  4207  copsex2g  4208  euotd  4216  onintrab2im  4479  mosubopt  4653  nfco  4753  dfdmf  4781  dfrnf  4829  nfdm  4832  fv3  5493  nfoprab2  5873  nfoprab3  5874  nfoprab  5875  cbvoprab1  5895  cbvoprab2  5896  cbvoprab3  5899  cnvoprab  6183  ac6sfi  6845  cc3  7190  nfsum1  11264  nfsum  11265  fsum2dlemstep  11342  nfcprod1  11462  nfcprod  11463  fprod2dlemstep  11530
  Copyright terms: Public domain W3C validator