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

Metamath Proof Explorer

Theorem cbvexv1

Description: Rule used to change bound variables, using implicit substitution. Version of cbvex with a disjoint variable condition, which does not require ax-13 . See cbvexvw for a version with two disjoint variable conditions, requiring fewer axioms, and cbvexv for another variant. (Contributed by NM, 21-Jun-1993) (Revised by BJ, 31-May-2019)

Ref Expression
Hypotheses cbvalv1.nf1 
|- F/ y ph
cbvalv1.nf2 
|- F/ x ps
cbvalv1.1 
|- ( x = y -> ( ph <-> ps ) )
Assertion cbvexv1 
|- ( E. x ph <-> E. y ps )

Proof

Step Hyp Ref Expression
1 cbvalv1.nf1 
 |-  F/ y ph
2 cbvalv1.nf2 
 |-  F/ x ps
3 cbvalv1.1 
 |-  ( x = y -> ( ph <-> ps ) )
4 1 nfn 
 |-  F/ y -. ph
5 2 nfn 
 |-  F/ x -. ps
6 3 notbid 
 |-  ( x = y -> ( -. ph <-> -. ps ) )
7 4 5 6 cbvalv1 
 |-  ( A. x -. ph <-> A. y -. ps )
8 alnex 
 |-  ( A. x -. ph <-> -. E. x ph )
9 alnex 
 |-  ( A. y -. ps <-> -. E. y ps )
10 7 8 9 3bitr3i 
 |-  ( -. E. x ph <-> -. E. y ps )
11 10 con4bii 
 |-  ( E. x ph <-> E. y ps )