Metamath Proof Explorer

Theorem ichbi12i

Description: Equivalence for interchangeable setvar variables. (Contributed by AV, 29-Jul-2023)

Ref Expression
Hypothesis ichbi12i.1 
|- ( ( x = a /\ y = b ) -> ( ps <-> ch ) )
Assertion ichbi12i 
|- ( [ x <> y ] ps <-> [ a <> b ] ch )

Proof

Step Hyp Ref Expression
1 ichbi12i.1 
 |-  ( ( x = a /\ y = b ) -> ( ps <-> ch ) )
2 nfv 
 |-  F/ b ps
3 2 sbco2v 
 |-  ( [ v / b ] [ b / y ] ps <-> [ v / y ] ps )
4 3 bicomi 
 |-  ( [ v / y ] ps <-> [ v / b ] [ b / y ] ps )
5 4 sbbii 
 |-  ( [ a / x ] [ v / y ] ps <-> [ a / x ] [ v / b ] [ b / y ] ps )
6 sbcom2 
 |-  ( [ a / x ] [ v / b ] [ b / y ] ps <-> [ v / b ] [ a / x ] [ b / y ] ps )
7 5 6 bitri 
 |-  ( [ a / x ] [ v / y ] ps <-> [ v / b ] [ a / x ] [ b / y ] ps )
8 7 sbbii 
 |-  ( [ u / a ] [ a / x ] [ v / y ] ps <-> [ u / a ] [ v / b ] [ a / x ] [ b / y ] ps )
9 nfv 
 |-  F/ a ps
10 9 nfsbv 
 |-  F/ a [ v / y ] ps
11 10 sbco2v 
 |-  ( [ u / a ] [ a / x ] [ v / y ] ps <-> [ u / x ] [ v / y ] ps )
12 1 2sbievw 
 |-  ( [ a / x ] [ b / y ] ps <-> ch )
13 12 2sbbii 
 |-  ( [ u / a ] [ v / b ] [ a / x ] [ b / y ] ps <-> [ u / a ] [ v / b ] ch )
14 8 11 13 3bitr3i 
 |-  ( [ u / x ] [ v / y ] ps <-> [ u / a ] [ v / b ] ch )
15 sbcom2 
 |-  ( [ u / b ] [ a / x ] [ b / y ] ps <-> [ a / x ] [ u / b ] [ b / y ] ps )
16 2 sbco2v 
 |-  ( [ u / b ] [ b / y ] ps <-> [ u / y ] ps )
17 16 sbbii 
 |-  ( [ a / x ] [ u / b ] [ b / y ] ps <-> [ a / x ] [ u / y ] ps )
18 15 17 bitri 
 |-  ( [ u / b ] [ a / x ] [ b / y ] ps <-> [ a / x ] [ u / y ] ps )
19 18 sbbii 
 |-  ( [ v / a ] [ u / b ] [ a / x ] [ b / y ] ps <-> [ v / a ] [ a / x ] [ u / y ] ps )
20 12 2sbbii 
 |-  ( [ v / a ] [ u / b ] [ a / x ] [ b / y ] ps <-> [ v / a ] [ u / b ] ch )
21 9 nfsbv 
 |-  F/ a [ u / y ] ps
22 21 sbco2v 
 |-  ( [ v / a ] [ a / x ] [ u / y ] ps <-> [ v / x ] [ u / y ] ps )
23 19 20 22 3bitr3ri 
 |-  ( [ v / x ] [ u / y ] ps <-> [ v / a ] [ u / b ] ch )
24 14 23 bibi12i 
 |-  ( ( [ u / x ] [ v / y ] ps <-> [ v / x ] [ u / y ] ps ) <-> ( [ u / a ] [ v / b ] ch <-> [ v / a ] [ u / b ] ch ) )
25 24 2albii 
 |-  ( A. u A. v ( [ u / x ] [ v / y ] ps <-> [ v / x ] [ u / y ] ps ) <-> A. u A. v ( [ u / a ] [ v / b ] ch <-> [ v / a ] [ u / b ] ch ) )
26 dfich2 
 |-  ( [ x <> y ] ps <-> A. u A. v ( [ u / x ] [ v / y ] ps <-> [ v / x ] [ u / y ] ps ) )
27 dfich2 
 |-  ( [ a <> b ] ch <-> A. u A. v ( [ u / a ] [ v / b ] ch <-> [ v / a ] [ u / b ] ch ) )
28 25 26 27 3bitr4i 
 |-  ( [ x <> y ] ps <-> [ a <> b ] ch )