Metamath Proof Explorer

Theorem dfich2

Description: Alternate definition of the propery of a wff ph that the setvar variables x and y are interchangeable. (Contributed by AV and WL, 6-Aug-2023)

Ref Expression
Assertion dfich2 
|- ( [ x <> y ] ph <-> A. a A. b ( [ a / x ] [ b / y ] ph <-> [ b / x ] [ a / y ] ph ) )

Proof

Step Hyp Ref Expression
1 df-ich 
 |-  ( [ x <> y ] ph <-> A. x A. y ( [ x / z ] [ y / x ] [ z / y ] ph <-> ph ) )
2 nfs1v 
 |-  F/ y [ b / y ] ph
3 2 nfsbv 
 |-  F/ y [ a / x ] [ b / y ] ph
4 3 nfsbv 
 |-  F/ y [ x / b ] [ a / x ] [ b / y ] ph
5 nfv 
 |-  F/ a ph
6 4 5 sbbib 
 |-  ( A. y ( [ y / a ] [ x / b ] [ a / x ] [ b / y ] ph <-> ph ) <-> A. a ( [ x / b ] [ a / x ] [ b / y ] ph <-> [ a / y ] ph ) )
7 6 albii 
 |-  ( A. x A. y ( [ y / a ] [ x / b ] [ a / x ] [ b / y ] ph <-> ph ) <-> A. x A. a ( [ x / b ] [ a / x ] [ b / y ] ph <-> [ a / y ] ph ) )
8 sbco4 
 |-  ( [ y / a ] [ x / b ] [ a / x ] [ b / y ] ph <-> [ x / z ] [ y / x ] [ z / y ] ph )
9 8 bibi1i 
 |-  ( ( [ y / a ] [ x / b ] [ a / x ] [ b / y ] ph <-> ph ) <-> ( [ x / z ] [ y / x ] [ z / y ] ph <-> ph ) )
10 9 2albii 
 |-  ( A. x A. y ( [ y / a ] [ x / b ] [ a / x ] [ b / y ] ph <-> ph ) <-> A. x A. y ( [ x / z ] [ y / x ] [ z / y ] ph <-> ph ) )
11 alcom 
 |-  ( A. x A. a ( [ x / b ] [ a / x ] [ b / y ] ph <-> [ a / y ] ph ) <-> A. a A. x ( [ x / b ] [ a / x ] [ b / y ] ph <-> [ a / y ] ph ) )
12 nfs1v 
 |-  F/ x [ a / x ] [ b / y ] ph
13 nfv 
 |-  F/ b [ a / y ] ph
14 12 13 sbbib 
 |-  ( A. x ( [ x / b ] [ a / x ] [ b / y ] ph <-> [ a / y ] ph ) <-> A. b ( [ a / x ] [ b / y ] ph <-> [ b / x ] [ a / y ] ph ) )
15 14 albii 
 |-  ( A. a A. x ( [ x / b ] [ a / x ] [ b / y ] ph <-> [ a / y ] ph ) <-> A. a A. b ( [ a / x ] [ b / y ] ph <-> [ b / x ] [ a / y ] ph ) )
16 11 15 bitri 
 |-  ( A. x A. a ( [ x / b ] [ a / x ] [ b / y ] ph <-> [ a / y ] ph ) <-> A. a A. b ( [ a / x ] [ b / y ] ph <-> [ b / x ] [ a / y ] ph ) )
17 7 10 16 3bitr3i 
 |-  ( A. x A. y ( [ x / z ] [ y / x ] [ z / y ] ph <-> ph ) <-> A. a A. b ( [ a / x ] [ b / y ] ph <-> [ b / x ] [ a / y ] ph ) )
18 1 17 bitri 
 |-  ( [ x <> y ] ph <-> A. a A. b ( [ a / x ] [ b / y ] ph <-> [ b / x ] [ a / y ] ph ) )