This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfreuw

Description: Bound-variable hypothesis builder for restricted unique existence. Version of nfreu with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 30-Oct-2010) Avoid ax-13 . (Revised by GG, 10-Jan-2024) Avoid ax-9 , ax-ext . (Revised by Wolf Lammen, 21-Nov-2024)

Ref Expression
Hypotheses nfrmow.1 
|- F/_ x A
nfrmow.2 
|- F/ x ph
Assertion nfreuw 
|- F/ x E! y e. A ph

Proof

Step Hyp Ref Expression
1 nfrmow.1 
 |-  F/_ x A
2 nfrmow.2 
 |-  F/ x ph
3 df-reu 
 |-  ( E! y e. A ph <-> E! y ( y e. A /\ ph ) )
4 1 nfcri 
 |-  F/ x y e. A
5 4 2 nfan 
 |-  F/ x ( y e. A /\ ph )
6 5 nfeuw 
 |-  F/ x E! y ( y e. A /\ ph )
7 3 6 nfxfr 
 |-  F/ x E! y e. A ph