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

Theorem nfex 1573
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 1457 . . 3 (𝜑 → ∀𝑥𝜑)
32hbex 1572 . 2 (∃𝑦𝜑 → ∀𝑥𝑦𝜑)
43nfi 1396 1 𝑥𝑦𝜑
Colors of variables: wff set class
Syntax hints:  wnf 1394  wex 1426
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445
This theorem depends on definitions:  df-bi 115  df-nf 1395
This theorem is referenced by:  eeor  1630  cbvex2  1845  eean  1854  nfeu1  1959  nfeuv  1966  nfel  2237  ceqsex2  2659  nfopab  3898  nfopab2  3900  cbvopab1  3903  cbvopab1s  3905  repizf2  3989  copsex2t  4063  copsex2g  4064  euotd  4072  onintrab2im  4325  mosubopt  4491  nfco  4589  dfdmf  4617  dfrnf  4664  nfdm  4667  fv3  5312  nfoprab2  5681  nfoprab3  5682  nfoprab  5683  cbvoprab1  5702  cbvoprab2  5703  cbvoprab3  5706  cnvoprab  5981  ac6sfi  6594  nfsum1  10709  nfsum  10710  fsum2dlemstep  10791
  Copyright terms: Public domain W3C validator