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

Theorem nfex 1599
 Description: If 𝑥 is not free in 𝜑, it is not free in ∃𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
Hypothesis
Ref Expression
nfex.1 𝑥𝜑
Assertion
Ref Expression
nfex 𝑥𝑦𝜑

Proof of Theorem nfex
StepHypRef Expression
1 nfex.1 . . . 4 𝑥𝜑
21nfri 1482 . . 3 (𝜑 → ∀𝑥𝜑)
32hbex 1598 . 2 (∃𝑦𝜑 → ∀𝑥𝑦𝜑)
43nfi 1421 1 𝑥𝑦𝜑
 Colors of variables: wff set class Syntax hints:  Ⅎwnf 1419  ∃wex 1451 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 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470 This theorem depends on definitions:  df-bi 116  df-nf 1420 This theorem is referenced by:  eeor  1656  cbvex2  1872  eean  1881  nfeu1  1986  nfeuv  1993  nfel  2265  ceqsex2  2698  nfopab  3964  nfopab2  3966  cbvopab1  3969  cbvopab1s  3971  repizf2  4054  copsex2t  4135  copsex2g  4136  euotd  4144  onintrab2im  4402  mosubopt  4572  nfco  4672  dfdmf  4700  dfrnf  4748  nfdm  4751  fv3  5410  nfoprab2  5787  nfoprab3  5788  nfoprab  5789  cbvoprab1  5809  cbvoprab2  5810  cbvoprab3  5813  cnvoprab  6097  ac6sfi  6758  nfsum1  11065  nfsum  11066  fsum2dlemstep  11143
 Copyright terms: Public domain W3C validator