Metamath Proof Explorer

Theorem ichal

Description: Move a universal quantifier inside interchangeability. (Contributed by SN, 30-Aug-2023)

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

Proof

Step Hyp Ref Expression
1 ax-11 
 |-  ( A. x A. a A. b ( [ a / u ] [ b / a ] [ u / b ] ph <-> ph ) -> A. a A. x A. b ( [ a / u ] [ b / a ] [ u / b ] ph <-> ph ) )
2 ax-11 
 |-  ( A. x A. b ( [ a / u ] [ b / a ] [ u / b ] ph <-> ph ) -> A. b A. x ( [ a / u ] [ b / a ] [ u / b ] ph <-> ph ) )
3 2 alimi 
 |-  ( A. a A. x A. b ( [ a / u ] [ b / a ] [ u / b ] ph <-> ph ) -> A. a A. b A. x ( [ a / u ] [ b / a ] [ u / b ] ph <-> ph ) )
4 sbal 
 |-  ( [ u / b ] A. x ph <-> A. x [ u / b ] ph )
5 4 2sbbii 
 |-  ( [ a / u ] [ b / a ] [ u / b ] A. x ph <-> [ a / u ] [ b / a ] A. x [ u / b ] ph )
6 sbal 
 |-  ( [ b / a ] A. x [ u / b ] ph <-> A. x [ b / a ] [ u / b ] ph )
7 6 sbbii 
 |-  ( [ a / u ] [ b / a ] A. x [ u / b ] ph <-> [ a / u ] A. x [ b / a ] [ u / b ] ph )
8 sbal 
 |-  ( [ a / u ] A. x [ b / a ] [ u / b ] ph <-> A. x [ a / u ] [ b / a ] [ u / b ] ph )
9 5 7 8 3bitri 
 |-  ( [ a / u ] [ b / a ] [ u / b ] A. x ph <-> A. x [ a / u ] [ b / a ] [ u / b ] ph )
10 albi 
 |-  ( A. x ( [ a / u ] [ b / a ] [ u / b ] ph <-> ph ) -> ( A. x [ a / u ] [ b / a ] [ u / b ] ph <-> A. x ph ) )
11 9 10 syl5bb 
 |-  ( A. x ( [ a / u ] [ b / a ] [ u / b ] ph <-> ph ) -> ( [ a / u ] [ b / a ] [ u / b ] A. x ph <-> A. x ph ) )
12 11 2alimi 
 |-  ( A. a A. b A. x ( [ a / u ] [ b / a ] [ u / b ] ph <-> ph ) -> A. a A. b ( [ a / u ] [ b / a ] [ u / b ] A. x ph <-> A. x ph ) )
13 1 3 12 3syl 
 |-  ( A. x A. a A. b ( [ a / u ] [ b / a ] [ u / b ] ph <-> ph ) -> A. a A. b ( [ a / u ] [ b / a ] [ u / b ] A. x ph <-> A. x ph ) )
14 df-ich 
 |-  ( [ a <> b ] ph <-> A. a A. b ( [ a / u ] [ b / a ] [ u / b ] ph <-> ph ) )
15 14 albii 
 |-  ( A. x [ a <> b ] ph <-> A. x A. a A. b ( [ a / u ] [ b / a ] [ u / b ] ph <-> ph ) )
16 df-ich 
 |-  ( [ a <> b ] A. x ph <-> A. a A. b ( [ a / u ] [ b / a ] [ u / b ] A. x ph <-> A. x ph ) )
17 13 15 16 3imtr4i 
 |-  ( A. x [ a <> b ] ph -> [ a <> b ] A. x ph )