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

Theorem nfex 1630
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 1512 . . 3  |-  ( ph  ->  A. x ph )
32hbex 1629 . 2  |-  ( E. y ph  ->  A. x E. y ph )
43nfi 1455 1  |-  F/ x E. y ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1453   E.wex 1485
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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503
This theorem depends on definitions:  df-bi 116  df-nf 1454
This theorem is referenced by:  eeor  1688  cbvexv1  1745  cbvex2  1915  eean  1924  nfsbv  1940  nfeu1  2030  nfeuv  2037  nfel  2321  ceqsex2  2770  nfopab  4057  nfopab2  4059  cbvopab1  4062  cbvopab1s  4064  repizf2  4148  copsex2t  4230  copsex2g  4231  euotd  4239  onintrab2im  4502  mosubopt  4676  nfco  4776  dfdmf  4804  dfrnf  4852  nfdm  4855  fv3  5519  nfoprab2  5903  nfoprab3  5904  nfoprab  5905  cbvoprab1  5925  cbvoprab2  5926  cbvoprab3  5929  cnvoprab  6213  ac6sfi  6876  cc3  7230  nfsum1  11319  nfsum  11320  fsum2dlemstep  11397  nfcprod1  11517  nfcprod  11518  fprod2dlemstep  11585
  Copyright terms: Public domain W3C validator