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

Theorem nfex 1635
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 1517 . . 3 (𝜑 → ∀𝑥𝜑)
32hbex 1634 . 2 (∃𝑦𝜑 → ∀𝑥𝑦𝜑)
43nfi 1460 1 𝑥𝑦𝜑
Colors of variables: wff set class
Syntax hints:  wnf 1458  wex 1490
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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-4 1508
This theorem depends on definitions:  df-bi 117  df-nf 1459
This theorem is referenced by:  eeor  1693  cbvexv1  1750  cbvex2  1920  eean  1929  nfsbv  1945  nfeu1  2035  nfeuv  2042  nfel  2326  ceqsex2  2775  nfopab  4066  nfopab2  4068  cbvopab1  4071  cbvopab1s  4073  repizf2  4157  copsex2t  4239  copsex2g  4240  euotd  4248  onintrab2im  4511  mosubopt  4685  nfco  4785  dfdmf  4813  dfrnf  4861  nfdm  4864  fv3  5530  nfoprab2  5915  nfoprab3  5916  nfoprab  5917  cbvoprab1  5937  cbvoprab2  5938  cbvoprab3  5941  cnvoprab  6225  ac6sfi  6888  cc3  7242  nfsum1  11331  nfsum  11332  fsum2dlemstep  11409  nfcprod1  11529  nfcprod  11530  fprod2dlemstep  11597
  Copyright terms: Public domain W3C validator