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

Metamath Proof Explorer

Theorem cbvmow

Description: Rule used to change bound variables, using implicit substitution. Version of cbvmo with a disjoint variable condition, which does not require ax-10 , ax-13 . (Contributed by NM, 9-Mar-1995) (Revised by GG, 23-May-2024)

Ref Expression
Hypotheses cbvmow.1 
|- F/ y ph
cbvmow.2 
|- F/ x ps
cbvmow.3 
|- ( x = y -> ( ph <-> ps ) )
Assertion cbvmow 
|- ( E* x ph <-> E* y ps )

Proof

Step Hyp Ref Expression
1 cbvmow.1 
 |-  F/ y ph
2 cbvmow.2 
 |-  F/ x ps
3 cbvmow.3 
 |-  ( x = y -> ( ph <-> ps ) )
4 nfv 
 |-  F/ y x = z
5 1 4 nfim 
 |-  F/ y ( ph -> x = z )
6 nfv 
 |-  F/ x y = z
7 2 6 nfim 
 |-  F/ x ( ps -> y = z )
8 equequ1 
 |-  ( x = y -> ( x = z <-> y = z ) )
9 3 8 imbi12d 
 |-  ( x = y -> ( ( ph -> x = z ) <-> ( ps -> y = z ) ) )
10 5 7 9 cbvalv1 
 |-  ( A. x ( ph -> x = z ) <-> A. y ( ps -> y = z ) )
11 10 exbii 
 |-  ( E. z A. x ( ph -> x = z ) <-> E. z A. y ( ps -> y = z ) )
12 df-mo 
 |-  ( E* x ph <-> E. z A. x ( ph -> x = z ) )
13 df-mo 
 |-  ( E* y ps <-> E. z A. y ( ps -> y = z ) )
14 11 12 13 3bitr4i 
 |-  ( E* x ph <-> E* y ps )