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

Metamath Proof Explorer

Theorem cbvralf

Description: Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvralfw when possible. (Contributed by NM, 7-Mar-2004) (Revised by Mario Carneiro, 9-Oct-2016) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cbvralf.1 
 |-  F/_ x A
2 cbvralf.2 
 |-  F/_ y A
3 cbvralf.3 
 |-  F/ y ph
4 cbvralf.4 
 |-  F/ x ps
5 cbvralf.5 
 |-  ( x = y -> ( ph <-> ps ) )
6 nfv 
 |-  F/ z ( x e. A -> ph )
7 1 nfcri 
 |-  F/ x z e. A
8 nfs1v 
 |-  F/ x [ z / x ] ph
9 7 8 nfim 
 |-  F/ x ( z e. A -> [ z / x ] ph )
10 eleq1w 
 |-  ( x = z -> ( x e. A <-> z e. A ) )
11 sbequ12 
 |-  ( x = z -> ( ph <-> [ z / x ] ph ) )
12 10 11 imbi12d 
 |-  ( x = z -> ( ( x e. A -> ph ) <-> ( z e. A -> [ z / x ] ph ) ) )
13 6 9 12 cbvalv1 
 |-  ( A. x ( x e. A -> ph ) <-> A. z ( z e. A -> [ z / x ] ph ) )
14 2 nfcri 
 |-  F/ y z e. A
15 3 nfsb 
 |-  F/ y [ z / x ] ph
16 14 15 nfim 
 |-  F/ y ( z e. A -> [ z / x ] ph )
17 nfv 
 |-  F/ z ( y e. A -> ps )
18 eleq1w 
 |-  ( z = y -> ( z e. A <-> y e. A ) )
19 sbequ 
 |-  ( z = y -> ( [ z / x ] ph <-> [ y / x ] ph ) )
20 4 5 sbie 
 |-  ( [ y / x ] ph <-> ps )
21 19 20 bitrdi 
 |-  ( z = y -> ( [ z / x ] ph <-> ps ) )
22 18 21 imbi12d 
 |-  ( z = y -> ( ( z e. A -> [ z / x ] ph ) <-> ( y e. A -> ps ) ) )
23 16 17 22 cbvalv1 
 |-  ( A. z ( z e. A -> [ z / x ] ph ) <-> A. y ( y e. A -> ps ) )
24 13 23 bitri 
 |-  ( A. x ( x e. A -> ph ) <-> A. y ( y e. A -> ps ) )
25 df-ral 
 |-  ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
26 df-ral 
 |-  ( A. y e. A ps <-> A. y ( y e. A -> ps ) )
27 24 25 26 3bitr4i 
 |-  ( A. x e. A ph <-> A. y e. A ps )