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

Metamath Proof Explorer

Theorem cbvrmow

Description: Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Version of cbvrmo with a disjoint variable condition, which does not require ax-10 , ax-13 . (Contributed by NM, 16-Jun-2017) Avoid ax-10 , ax-13 . (Revised by GG, 23-May-2024)

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

Proof

Step Hyp Ref Expression
1 cbvrmow.1 
 |-  F/ y ph
2 cbvrmow.2 
 |-  F/ x ps
3 cbvrmow.3 
 |-  ( x = y -> ( ph <-> ps ) )
4 nfv 
 |-  F/ y x e. A
5 4 1 nfan 
 |-  F/ y ( x e. A /\ ph )
6 nfv 
 |-  F/ x y e. A
7 6 2 nfan 
 |-  F/ x ( y e. A /\ ps )
8 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
9 8 3 anbi12d 
 |-  ( x = y -> ( ( x e. A /\ ph ) <-> ( y e. A /\ ps ) ) )
10 5 7 9 cbvmow 
 |-  ( E* x ( x e. A /\ ph ) <-> E* y ( y e. A /\ ps ) )
11 df-rmo 
 |-  ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
12 df-rmo 
 |-  ( E* y e. A ps <-> E* y ( y e. A /\ ps ) )
13 10 11 12 3bitr4i 
 |-  ( E* x e. A ph <-> E* y e. A ps )