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

Metamath Proof Explorer

Theorem cbval2v

Description: Rule used to change bound variables, using implicit substitution. Version of cbval2 with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 22-Dec-2003) (Revised by BJ, 16-Jun-2019) (Proof shortened by GG, 10-Jan-2024)

Ref Expression
Hypotheses cbval2v.1 
|- F/ z ph
cbval2v.2 
|- F/ w ph
cbval2v.3 
|- F/ x ps
cbval2v.4 
|- F/ y ps
cbval2v.5 
|- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )
Assertion cbval2v 
|- ( A. x A. y ph <-> A. z A. w ps )

Proof

Step Hyp Ref Expression
1 cbval2v.1 
 |-  F/ z ph
2 cbval2v.2 
 |-  F/ w ph
3 cbval2v.3 
 |-  F/ x ps
4 cbval2v.4 
 |-  F/ y ps
5 cbval2v.5 
 |-  ( ( x = z /\ y = w ) -> ( ph <-> ps ) )
6 1 nfal 
 |-  F/ z A. y ph
7 3 nfal 
 |-  F/ x A. w ps
8 nfv 
 |-  F/ y x = z
9 nfv 
 |-  F/ w x = z
10 2 a1i 
 |-  ( x = z -> F/ w ph )
11 4 a1i 
 |-  ( x = z -> F/ y ps )
12 5 ex 
 |-  ( x = z -> ( y = w -> ( ph <-> ps ) ) )
13 8 9 10 11 12 cbv2w 
 |-  ( x = z -> ( A. y ph <-> A. w ps ) )
14 6 7 13 cbvalv1 
 |-  ( A. x A. y ph <-> A. z A. w ps )