Theorem nfrmo1 2539

Description: 𝑥 is not free in ∃*𝑥 ∈ 𝐴𝜑. (Contributed by NM, 16-Jun-2017.)

Assertion

Ref	Expression
nfrmo1	⊢ Ⅎ𝑥∃*𝑥 ∈ 𝐴 𝜑

Proof of Theorem nfrmo1

Step	Hyp	Ref	Expression
1		df-rmo 2367	. 2 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
2		nfmo1 1960	. 2 ⊢ Ⅎ𝑥∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
3	1, 2	nfxfr 1408	1 ⊢ Ⅎ𝑥∃*𝑥 ∈ 𝐴 𝜑

Syntax hints:   ∧ wa 102  Ⅎwnf 1394   ∈ wcel 1438  ∃*wmo 1949  ∃*wrmo 2362

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  ax-ial 1472  ax-i5r 1473

This theorem depends on definitions:  df-bi 115  df-nf 1395  df-eu 1951  df-mo 1952  df-rmo 2367

This theorem is referenced by:  nfdisj1  3835