Metamath Proof Explorer


Theorem cbvmowOLD

Description: Obsolete version of cbvmow as of 23-May-2024. (Contributed by NM, 9-Mar-1995) (Revised by Gino Giotto, 10-Jan-2024) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cbvmowOLD.1
 |-  F/ y ph
2 cbvmowOLD.2
 |-  F/ x ps
3 cbvmowOLD.3
 |-  ( x = y -> ( ph <-> ps ) )
4 1 sb8ev
 |-  ( E. x ph <-> E. y [ y / x ] ph )
5 1 sb8euv
 |-  ( E! x ph <-> E! y [ y / x ] ph )
6 4 5 imbi12i
 |-  ( ( E. x ph -> E! x ph ) <-> ( E. y [ y / x ] ph -> E! y [ y / x ] ph ) )
7 moeu
 |-  ( E* x ph <-> ( E. x ph -> E! x ph ) )
8 moeu
 |-  ( E* y [ y / x ] ph <-> ( E. y [ y / x ] ph -> E! y [ y / x ] ph ) )
9 6 7 8 3bitr4i
 |-  ( E* x ph <-> E* y [ y / x ] ph )
10 2 3 sbiev
 |-  ( [ y / x ] ph <-> ps )
11 10 mobii
 |-  ( E* y [ y / x ] ph <-> E* y ps )
12 9 11 bitri
 |-  ( E* x ph <-> E* y ps )