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

Metamath Proof Explorer

Theorem ichnfim

Description: If in an interchangeability context x is not free in ph , the same holds for y . (Contributed by Wolf Lammen, 6-Aug-2023) (Revised by AV, 23-Sep-2023)

Ref Expression
Assertion ichnfim 
|- ( ( A. y F/ x ph /\ [ x <> y ] ph ) -> A. x F/ y ph )

Proof

Step Hyp Ref Expression
1 nfnf1 
 |-  F/ x F/ x ph
2 1 nfal 
 |-  F/ x A. y F/ x ph
3 nfich1 
 |-  F/ x [ x <> y ] ph
4 2 3 nfan 
 |-  F/ x ( A. y F/ x ph /\ [ x <> y ] ph )
5 dfich2 
 |-  ( [ x <> y ] ph <-> A. a A. b ( [ a / x ] [ b / y ] ph <-> [ b / x ] [ a / y ] ph ) )
6 ichnfimlem 
 |-  ( A. y F/ x ph -> ( [ a / x ] [ b / y ] ph <-> [ b / y ] ph ) )
7 ichnfimlem 
 |-  ( A. y F/ x ph -> ( [ b / x ] [ a / y ] ph <-> [ a / y ] ph ) )
8 6 7 bibi12d 
 |-  ( A. y F/ x ph -> ( ( [ a / x ] [ b / y ] ph <-> [ b / x ] [ a / y ] ph ) <-> ( [ b / y ] ph <-> [ a / y ] ph ) ) )
9 bicom1 
 |-  ( ( [ b / y ] ph <-> [ a / y ] ph ) -> ( [ a / y ] ph <-> [ b / y ] ph ) )
10 8 9 biimtrdi 
 |-  ( A. y F/ x ph -> ( ( [ a / x ] [ b / y ] ph <-> [ b / x ] [ a / y ] ph ) -> ( [ a / y ] ph <-> [ b / y ] ph ) ) )
11 10 2alimdv 
 |-  ( A. y F/ x ph -> ( A. a A. b ( [ a / x ] [ b / y ] ph <-> [ b / x ] [ a / y ] ph ) -> A. a A. b ( [ a / y ] ph <-> [ b / y ] ph ) ) )
12 5 11 biimtrid 
 |-  ( A. y F/ x ph -> ( [ x <> y ] ph -> A. a A. b ( [ a / y ] ph <-> [ b / y ] ph ) ) )
13 12 imp 
 |-  ( ( A. y F/ x ph /\ [ x <> y ] ph ) -> A. a A. b ( [ a / y ] ph <-> [ b / y ] ph ) )
14 sbnf2 
 |-  ( F/ y ph <-> A. a A. b ( [ a / y ] ph <-> [ b / y ] ph ) )
15 13 14 sylibr 
 |-  ( ( A. y F/ x ph /\ [ x <> y ] ph ) -> F/ y ph )
16 4 15 alrimi 
 |-  ( ( A. y F/ x ph /\ [ x <> y ] ph ) -> A. x F/ y ph )