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

Metamath Proof Explorer

Theorem sbnf

Description: Move nonfree predicate in and out of substitution; see sbal and sbex . (Contributed by BJ, 2-May-2019) (Proof shortened by Wolf Lammen, 2-May-2025)

Ref Expression
Assertion sbnf 
|- ( [ z / y ] F/ x ph <-> F/ x [ z / y ] ph )

Proof

Step Hyp Ref Expression
1 df-nf 
 |-  ( F/ x ph <-> ( E. x ph -> A. x ph ) )
2 1 sbbii 
 |-  ( [ z / y ] F/ x ph <-> [ z / y ] ( E. x ph -> A. x ph ) )
3 sbim 
 |-  ( [ z / y ] ( E. x ph -> A. x ph ) <-> ( [ z / y ] E. x ph -> [ z / y ] A. x ph ) )
4 sbex 
 |-  ( [ z / y ] E. x ph <-> E. x [ z / y ] ph )
5 sbal 
 |-  ( [ z / y ] A. x ph <-> A. x [ z / y ] ph )
6 4 5 imbi12i 
 |-  ( ( [ z / y ] E. x ph -> [ z / y ] A. x ph ) <-> ( E. x [ z / y ] ph -> A. x [ z / y ] ph ) )
7 df-nf 
 |-  ( F/ x [ z / y ] ph <-> ( E. x [ z / y ] ph -> A. x [ z / y ] ph ) )
8 6 7 bitr4i 
 |-  ( ( [ z / y ] E. x ph -> [ z / y ] A. x ph ) <-> F/ x [ z / y ] ph )
9 2 3 8 3bitri 
 |-  ( [ z / y ] F/ x ph <-> F/ x [ z / y ] ph )