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

Metamath Proof Explorer

Theorem reu8nf

Description: Restricted uniqueness using implicit substitution. This version of reu8 uses a nonfreeness hypothesis for x and ps instead of distinct variable conditions. (Contributed by AV, 21-Jan-2022)

Ref Expression
Hypotheses reu8nf.1 
|- F/ x ps
reu8nf.2 
|- F/ x ch
reu8nf.3 
|- ( x = w -> ( ph <-> ch ) )
reu8nf.4 
|- ( w = y -> ( ch <-> ps ) )
Assertion reu8nf 
|- ( E! x e. A ph <-> E. x e. A ( ph /\ A. y e. A ( ps -> x = y ) ) )

Proof

Step Hyp Ref Expression
1 reu8nf.1 
 |-  F/ x ps
2 reu8nf.2 
 |-  F/ x ch
3 reu8nf.3 
 |-  ( x = w -> ( ph <-> ch ) )
4 reu8nf.4 
 |-  ( w = y -> ( ch <-> ps ) )
5 nfv 
 |-  F/ w ph
6 5 2 3 cbvreuw 
 |-  ( E! x e. A ph <-> E! w e. A ch )
7 4 reu8 
 |-  ( E! w e. A ch <-> E. w e. A ( ch /\ A. y e. A ( ps -> w = y ) ) )
8 nfcv 
 |-  F/_ x A
9 nfv 
 |-  F/ x w = y
10 1 9 nfim 
 |-  F/ x ( ps -> w = y )
11 8 10 nfralw 
 |-  F/ x A. y e. A ( ps -> w = y )
12 2 11 nfan 
 |-  F/ x ( ch /\ A. y e. A ( ps -> w = y ) )
13 nfv 
 |-  F/ w ( ph /\ A. y e. A ( ps -> x = y ) )
14 3 bicomd 
 |-  ( x = w -> ( ch <-> ph ) )
15 14 equcoms 
 |-  ( w = x -> ( ch <-> ph ) )
16 equequ1 
 |-  ( w = x -> ( w = y <-> x = y ) )
17 16 imbi2d 
 |-  ( w = x -> ( ( ps -> w = y ) <-> ( ps -> x = y ) ) )
18 17 ralbidv 
 |-  ( w = x -> ( A. y e. A ( ps -> w = y ) <-> A. y e. A ( ps -> x = y ) ) )
19 15 18 anbi12d 
 |-  ( w = x -> ( ( ch /\ A. y e. A ( ps -> w = y ) ) <-> ( ph /\ A. y e. A ( ps -> x = y ) ) ) )
20 12 13 19 cbvrexw 
 |-  ( E. w e. A ( ch /\ A. y e. A ( ps -> w = y ) ) <-> E. x e. A ( ph /\ A. y e. A ( ps -> x = y ) ) )
21 6 7 20 3bitri 
 |-  ( E! x e. A ph <-> E. x e. A ( ph /\ A. y e. A ( ps -> x = y ) ) )