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

Theorem nfre1 2415
Description: 𝑥 is not free in 𝑥𝐴𝜑. (Contributed by NM, 19-Mar-1997.) (Revised by Mario Carneiro, 7-Oct-2016.)
Assertion
Ref Expression
nfre1 𝑥𝑥𝐴 𝜑

Proof of Theorem nfre1
StepHypRef Expression
1 df-rex 2361 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
2 nfe1 1428 . 2 𝑥𝑥(𝑥𝐴𝜑)
31, 2nfxfr 1406 1 𝑥𝑥𝐴 𝜑
Colors of variables: wff set class
Syntax hints:  wa 102  wnf 1392  wex 1424  wcel 1436  wrex 2356
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 1379  ax-gen 1381  ax-ie1 1425
This theorem depends on definitions:  df-bi 115  df-nf 1393  df-rex 2361
This theorem is referenced by:  nfiu1  3737  fun11iun  5225  eusvobj2  5580  fodjuomnilemdc  6720  prarloclem3step  6976  prmuloc2  7047  ltexprlemm  7080  caucvgprprlemaddq  7188  caucvgsrlemgt1  7261  supinfneg  8992  infsupneg  8993  lbzbi  9010  divalglemeunn  10715  divalglemeuneg  10717  bezoutlemmain  10781  bezout  10794
  Copyright terms: Public domain W3C validator