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

Theorem nfex 1637
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 1519 . . 3 (𝜑 → ∀𝑥𝜑)
32hbex 1636 . 2 (∃𝑦𝜑 → ∀𝑥𝑦𝜑)
43nfi 1462 1 𝑥𝑦𝜑
Colors of variables: wff set class
Syntax hints:  wnf 1460  wex 1492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510
This theorem depends on definitions:  df-bi 117  df-nf 1461
This theorem is referenced by:  eeor  1695  cbvexv1  1752  cbvex2  1922  eean  1931  nfsbv  1947  nfeu1  2037  nfeuv  2044  nfel  2328  ceqsex2  2778  nfopab  4072  nfopab2  4074  cbvopab1  4077  cbvopab1s  4079  repizf2  4163  copsex2t  4246  copsex2g  4247  euotd  4255  onintrab2im  4518  mosubopt  4692  nfco  4793  dfdmf  4821  dfrnf  4869  nfdm  4872  fv3  5539  nfoprab2  5925  nfoprab3  5926  nfoprab  5927  cbvoprab1  5947  cbvoprab2  5948  cbvoprab3  5951  cnvoprab  6235  ac6sfi  6898  cc3  7267  nfsum1  11364  nfsum  11365  fsum2dlemstep  11442  nfcprod1  11562  nfcprod  11563  fprod2dlemstep  11630
  Copyright terms: Public domain W3C validator