Metamath Proof Explorer


Theorem cbval2vOLD

Description: Obsolete version of cbval2v as of 14-Jan-2024. (Contributed by BJ, 16-Jan-2019) (Proof modification is discouraged.) (New usage is discouraged.)

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 cbval2vOLD
|- ( 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/ w x = z
9 8 2 nfim
 |-  F/ w ( x = z -> ph )
10 nfv
 |-  F/ y x = z
11 10 4 nfim
 |-  F/ y ( x = z -> ps )
12 5 expcom
 |-  ( y = w -> ( x = z -> ( ph <-> ps ) ) )
13 12 pm5.74d
 |-  ( y = w -> ( ( x = z -> ph ) <-> ( x = z -> ps ) ) )
14 9 11 13 cbvalv1
 |-  ( A. y ( x = z -> ph ) <-> A. w ( x = z -> ps ) )
15 19.21v
 |-  ( A. y ( x = z -> ph ) <-> ( x = z -> A. y ph ) )
16 19.21v
 |-  ( A. w ( x = z -> ps ) <-> ( x = z -> A. w ps ) )
17 14 15 16 3bitr3i
 |-  ( ( x = z -> A. y ph ) <-> ( x = z -> A. w ps ) )
18 17 pm5.74ri
 |-  ( x = z -> ( A. y ph <-> A. w ps ) )
19 6 7 18 cbvalv1
 |-  ( A. x A. y ph <-> A. z A. w ps )