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 Gino Giotto, 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 )