MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfex Structured version   Visualization version   Unicode version

Theorem nfex 2031
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
nfal.1  |-  F/ x ph
Assertion
Ref Expression
nfex  |-  F/ x E. y ph

Proof of Theorem nfex
StepHypRef Expression
1 nfal.1 . . . 4  |-  F/ x ph
21nfri 1952 . . 3  |-  ( ph  ->  A. x ph )
32hbex 2029 . 2  |-  ( E. y ph  ->  A. x E. y ph )
43nfi 1674 1  |-  F/ x E. y ph
Colors of variables: wff setvar class
Syntax hints:   E.wex 1663   F/wnf 1667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-nf 1668
This theorem is referenced by:  19.12  2033  eeor  2056  eean  2077  eeeanv  2079  nfeu1  2309  moexex  2370  ceqsex2  3086  nfopab  4468  nfopab2  4470  cbvopab1  4473  cbvopab1s  4475  axrep2  4517  axrep3  4518  axrep4  4519  copsex2t  4688  copsex2g  4689  mosubopt  4699  euotd  4702  nfco  5000  dfdmf  5028  dfrnf  5073  nfdm  5076  fv3  5878  oprabv  6339  nfoprab2  6341  nfoprab3  6342  nfoprab  6343  cbvoprab1  6363  cbvoprab2  6364  cbvoprab3  6367  nfwrecs  7030  ac6sfi  7815  aceq1  8548  zfcndrep  9039  zfcndinf  9043  nfsum1  13756  nfsum  13757  fsum2dlem  13831  nfcprod1  13964  nfcprod  13965  fprod2dlem  14034  brabgaf  28216  cnvoprab  28308  bnj981  29761  bnj1388  29842  bnj1445  29853  bnj1489  29865  bj-axrep2  31404  bj-axrep3  31405  bj-axrep4  31406  pm11.71  36747  upbdrech  37523  stoweidlem57  37918
  Copyright terms: Public domain W3C validator