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

Metamath Proof Explorer

Theorem cbvreu

Description: Change the bound variable of a restricted unique existential quantifier using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvreuw when possible. (Contributed by Mario Carneiro, 15-Oct-2016) (New usage is discouraged.)

Ref Expression
Hypotheses cbvrmo.1 
|- F/ y ph
cbvrmo.2 
|- F/ x ps
cbvrmo.3 
|- ( x = y -> ( ph <-> ps ) )
Assertion cbvreu 
|- ( E! x e. A ph <-> E! y e. A ps )

Proof

Step Hyp Ref Expression
1 cbvrmo.1 
 |-  F/ y ph
2 cbvrmo.2 
 |-  F/ x ps
3 cbvrmo.3 
 |-  ( x = y -> ( ph <-> ps ) )
4 nfv 
 |-  F/ z ( x e. A /\ ph )
5 4 sb8eu 
 |-  ( E! x ( x e. A /\ ph ) <-> E! z [ z / x ] ( x e. A /\ ph ) )
6 sban 
 |-  ( [ z / x ] ( x e. A /\ ph ) <-> ( [ z / x ] x e. A /\ [ z / x ] ph ) )
7 6 eubii 
 |-  ( E! z [ z / x ] ( x e. A /\ ph ) <-> E! z ( [ z / x ] x e. A /\ [ z / x ] ph ) )
8 clelsb1 
 |-  ( [ z / x ] x e. A <-> z e. A )
9 8 anbi1i 
 |-  ( ( [ z / x ] x e. A /\ [ z / x ] ph ) <-> ( z e. A /\ [ z / x ] ph ) )
10 9 eubii 
 |-  ( E! z ( [ z / x ] x e. A /\ [ z / x ] ph ) <-> E! z ( z e. A /\ [ z / x ] ph ) )
11 nfv 
 |-  F/ y z e. A
12 1 nfsb 
 |-  F/ y [ z / x ] ph
13 11 12 nfan 
 |-  F/ y ( z e. A /\ [ z / x ] ph )
14 nfv 
 |-  F/ z ( y e. A /\ ps )
15 eleq1w 
 |-  ( z = y -> ( z e. A <-> y e. A ) )
16 sbequ 
 |-  ( z = y -> ( [ z / x ] ph <-> [ y / x ] ph ) )
17 2 3 sbie 
 |-  ( [ y / x ] ph <-> ps )
18 16 17 bitrdi 
 |-  ( z = y -> ( [ z / x ] ph <-> ps ) )
19 15 18 anbi12d 
 |-  ( z = y -> ( ( z e. A /\ [ z / x ] ph ) <-> ( y e. A /\ ps ) ) )
20 13 14 19 cbveu 
 |-  ( E! z ( z e. A /\ [ z / x ] ph ) <-> E! y ( y e. A /\ ps ) )
21 10 20 bitri 
 |-  ( E! z ( [ z / x ] x e. A /\ [ z / x ] ph ) <-> E! y ( y e. A /\ ps ) )
22 5 7 21 3bitri 
 |-  ( E! x ( x e. A /\ ph ) <-> E! y ( y e. A /\ ps ) )
23 df-reu 
 |-  ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
24 df-reu 
 |-  ( E! y e. A ps <-> E! y ( y e. A /\ ps ) )
25 22 23 24 3bitr4i 
 |-  ( E! x e. A ph <-> E! y e. A ps )