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

Metamath Proof Explorer

Theorem cbvralcsf

Description: A more general version of cbvralf that doesn't require A and B to be distinct from x or y . Changes bound variables using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Andrew Salmon, 13-Jul-2011) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cbvralcsf.1 
 |-  F/_ y A
2 cbvralcsf.2 
 |-  F/_ x B
3 cbvralcsf.3 
 |-  F/ y ph
4 cbvralcsf.4 
 |-  F/ x ps
5 cbvralcsf.5 
 |-  ( x = y -> A = B )
6 cbvralcsf.6 
 |-  ( x = y -> ( ph <-> ps ) )
7 nfv 
 |-  F/ z ( x e. A -> ph )
8 nfcsb1v 
 |-  F/_ x [_ z / x ]_ A
9 8 nfcri 
 |-  F/ x z e. [_ z / x ]_ A
10 nfsbc1v 
 |-  F/ x [. z / x ]. ph
11 9 10 nfim 
 |-  F/ x ( z e. [_ z / x ]_ A -> [. z / x ]. ph )
12 id 
 |-  ( x = z -> x = z )
13 csbeq1a 
 |-  ( x = z -> A = [_ z / x ]_ A )
14 12 13 eleq12d 
 |-  ( x = z -> ( x e. A <-> z e. [_ z / x ]_ A ) )
15 sbceq1a 
 |-  ( x = z -> ( ph <-> [. z / x ]. ph ) )
16 14 15 imbi12d 
 |-  ( x = z -> ( ( x e. A -> ph ) <-> ( z e. [_ z / x ]_ A -> [. z / x ]. ph ) ) )
17 7 11 16 cbvalv1 
 |-  ( A. x ( x e. A -> ph ) <-> A. z ( z e. [_ z / x ]_ A -> [. z / x ]. ph ) )
18 nfcv 
 |-  F/_ y z
19 18 1 nfcsb 
 |-  F/_ y [_ z / x ]_ A
20 19 nfcri 
 |-  F/ y z e. [_ z / x ]_ A
21 18 3 nfsbc 
 |-  F/ y [. z / x ]. ph
22 20 21 nfim 
 |-  F/ y ( z e. [_ z / x ]_ A -> [. z / x ]. ph )
23 nfv 
 |-  F/ z ( y e. B -> ps )
24 id 
 |-  ( z = y -> z = y )
25 csbeq1 
 |-  ( z = y -> [_ z / x ]_ A = [_ y / x ]_ A )
26 df-csb 
 |-  [_ y / x ]_ A = { v | [. y / x ]. v e. A }
27 2 nfcri 
 |-  F/ x v e. B
28 5 eleq2d 
 |-  ( x = y -> ( v e. A <-> v e. B ) )
29 27 28 sbie 
 |-  ( [ y / x ] v e. A <-> v e. B )
30 sbsbc 
 |-  ( [ y / x ] v e. A <-> [. y / x ]. v e. A )
31 29 30 bitr3i 
 |-  ( v e. B <-> [. y / x ]. v e. A )
32 31 eqabi 
 |-  B = { v | [. y / x ]. v e. A }
33 26 32 eqtr4i 
 |-  [_ y / x ]_ A = B
34 25 33 eqtrdi 
 |-  ( z = y -> [_ z / x ]_ A = B )
35 24 34 eleq12d 
 |-  ( z = y -> ( z e. [_ z / x ]_ A <-> y e. B ) )
36 dfsbcq 
 |-  ( z = y -> ( [. z / x ]. ph <-> [. y / x ]. ph ) )
37 sbsbc 
 |-  ( [ y / x ] ph <-> [. y / x ]. ph )
38 4 6 sbie 
 |-  ( [ y / x ] ph <-> ps )
39 37 38 bitr3i 
 |-  ( [. y / x ]. ph <-> ps )
40 36 39 bitrdi 
 |-  ( z = y -> ( [. z / x ]. ph <-> ps ) )
41 35 40 imbi12d 
 |-  ( z = y -> ( ( z e. [_ z / x ]_ A -> [. z / x ]. ph ) <-> ( y e. B -> ps ) ) )
42 22 23 41 cbvalv1 
 |-  ( A. z ( z e. [_ z / x ]_ A -> [. z / x ]. ph ) <-> A. y ( y e. B -> ps ) )
43 17 42 bitri 
 |-  ( A. x ( x e. A -> ph ) <-> A. y ( y e. B -> ps ) )
44 df-ral 
 |-  ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
45 df-ral 
 |-  ( A. y e. B ps <-> A. y ( y e. B -> ps ) )
46 43 44 45 3bitr4i 
 |-  ( A. x e. A ph <-> A. y e. B ps )