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

Step	Hyp	Ref	Expression
1		df-rex 2361	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
2		nfe1 1428	. 2 ⊢ Ⅎ𝑥∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
3	1, 2	nfxfr 1406	1 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑

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