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

Theorem nfex 1544
 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 1428 . . 3 (𝜑 → ∀𝑥𝜑)
32hbex 1543 . 2 (∃𝑦𝜑 → ∀𝑥𝑦𝜑)
43nfi 1367 1 𝑥𝑦𝜑
 Colors of variables: wff set class Syntax hints:  Ⅎwnf 1365  ∃wex 1397 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416 This theorem depends on definitions:  df-bi 114  df-nf 1366 This theorem is referenced by:  eeor  1601  cbvex2  1813  eean  1822  nfeu1  1927  nfeuv  1934  nfel  2202  ceqsex2  2611  nfopab  3853  nfopab2  3855  cbvopab1  3858  cbvopab1s  3860  repizf2  3943  copsex2t  4010  copsex2g  4011  euotd  4019  onintrab2im  4272  mosubopt  4433  nfco  4529  dfdmf  4556  dfrnf  4603  nfdm  4606  fv3  5225  nfoprab2  5583  nfoprab3  5584  nfoprab  5585  cbvoprab1  5604  cbvoprab2  5605  cbvoprab3  5608  cnvoprab  5883  ac6sfi  6383  nfsum1  10106  nfsum  10107
 Copyright terms: Public domain W3C validator