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

Metamath Proof Explorer

Theorem cbvrexfw

Description: Rule used to change bound variables, using implicit substitution. Version of cbvrexf with a disjoint variable condition, which does not require ax-13 . For a version not dependent on ax-11 and ax-12, see cbvrexvw . (Contributed by FL, 27-Apr-2008) Avoid ax-10 , ax-13 . (Revised by GG, 10-Jan-2024)

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

Proof

Step Hyp Ref Expression
1 cbvrexfw.1 
 |-  F/_ x A
2 cbvrexfw.2 
 |-  F/_ y A
3 cbvrexfw.3 
 |-  F/ y ph
4 cbvrexfw.4 
 |-  F/ x ps
5 cbvrexfw.5 
 |-  ( x = y -> ( ph <-> ps ) )
6 3 nfn 
 |-  F/ y -. ph
7 4 nfn 
 |-  F/ x -. ps
8 5 notbid 
 |-  ( x = y -> ( -. ph <-> -. ps ) )
9 1 2 6 7 8 cbvralfw 
 |-  ( A. x e. A -. ph <-> A. y e. A -. ps )
10 ralnex 
 |-  ( A. x e. A -. ph <-> -. E. x e. A ph )
11 ralnex 
 |-  ( A. y e. A -. ps <-> -. E. y e. A ps )
12 9 10 11 3bitr3i 
 |-  ( -. E. x e. A ph <-> -. E. y e. A ps )
13 12 con4bii 
 |-  ( E. x e. A ph <-> E. y e. A ps )