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

Metamath Proof Explorer

Theorem 2mosOLD

Description: Obsolete version of 2mos as of 21-May-2025. (Contributed by NM, 10-Feb-2005) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis 2mos.1 
|- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )
Assertion 2mosOLD 
|- ( E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) <-> A. x A. y A. z A. w ( ( ph /\ ps ) -> ( x = z /\ y = w ) ) )

Proof

Step Hyp Ref Expression
1 2mos.1 
 |-  ( ( x = z /\ y = w ) -> ( ph <-> ps ) )
2 2mo 
 |-  ( E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) <-> A. x A. y A. z A. w ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) )
3 nfv 
 |-  F/ y x = z
4 3 sbrim 
 |-  ( [ w / y ] ( x = z -> ph ) <-> ( x = z -> [ w / y ] ph ) )
5 1 expcom 
 |-  ( y = w -> ( x = z -> ( ph <-> ps ) ) )
6 5 pm5.74d 
 |-  ( y = w -> ( ( x = z -> ph ) <-> ( x = z -> ps ) ) )
7 6 sbievw 
 |-  ( [ w / y ] ( x = z -> ph ) <-> ( x = z -> ps ) )
8 4 7 bitr3i 
 |-  ( ( x = z -> [ w / y ] ph ) <-> ( x = z -> ps ) )
9 8 pm5.74ri 
 |-  ( x = z -> ( [ w / y ] ph <-> ps ) )
10 9 sbievw 
 |-  ( [ z / x ] [ w / y ] ph <-> ps )
11 10 anbi2i 
 |-  ( ( ph /\ [ z / x ] [ w / y ] ph ) <-> ( ph /\ ps ) )
12 11 imbi1i 
 |-  ( ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) <-> ( ( ph /\ ps ) -> ( x = z /\ y = w ) ) )
13 12 2albii 
 |-  ( A. z A. w ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) <-> A. z A. w ( ( ph /\ ps ) -> ( x = z /\ y = w ) ) )
14 13 2albii 
 |-  ( A. x A. y A. z A. w ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) <-> A. x A. y A. z A. w ( ( ph /\ ps ) -> ( x = z /\ y = w ) ) )
15 2 14 bitri 
 |-  ( E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) <-> A. x A. y A. z A. w ( ( ph /\ ps ) -> ( x = z /\ y = w ) ) )