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

Theorem nfex 1886
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 1813 . . 3  |-  ( ph  ->  A. x ph )
32hbex 1884 . 2  |-  ( E. y ph  ->  A. x E. y ph )
43nfi 1597 1  |-  F/ x E. y ph
Colors of variables: wff setvar class
Syntax hints:   E.wex 1587   F/wnf 1590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-ex 1588  df-nf 1591
This theorem is referenced by:  19.12  1888  eeor  1916  eean  1943  eeeanv  1945  cbvex2OLD  1989  nfeu1  2275  moexex  2358  moexexOLD  2359  nfelOLD  2630  ceqsex2  3116  nfopab  4468  nfopab2  4470  cbvopab1  4473  cbvopab1s  4475  axrep2  4516  axrep3  4517  axrep4  4518  copsex2t  4689  copsex2g  4690  mosubopt  4700  euotd  4703  nfco  5116  dfdmf  5144  dfrnf  5189  nfdm  5192  fv3  5815  nfoprab2  6248  nfoprab3  6249  nfoprab  6250  cbvoprab1  6270  cbvoprab2  6271  cbvoprab3  6274  ac6sfi  7670  aceq1  8402  zfcndrep  8896  zfcndinf  8900  nfsum1  13289  nfsum  13290  fsum2dlem  13359  cnvoprab  26201  nfcprod1  27590  nfcprod  27591  fprod2dlem  27658  nfwrecs  27886  pm11.71  29821  stoweidlem57  30023  oprabv  30328  bnj981  32298  bnj1388  32379  bnj1445  32390  bnj1489  32402  bj-axrep2  32667  bj-axrep3  32668  bj-axrep4  32669
  Copyright terms: Public domain W3C validator