Metamath Proof Explorer

Theorem sbex

Description: Move existential quantifier in and out of substitution. (Contributed by NM, 27-Sep-2003)

Ref Expression
Assertion sbex 
|- ( [ z / y ] E. x ph <-> E. x [ z / y ] ph )

Proof

Step Hyp Ref Expression
1 sbn 
 |-  ( [ z / y ] -. A. x -. ph <-> -. [ z / y ] A. x -. ph )
2 sbn 
 |-  ( [ z / y ] -. ph <-> -. [ z / y ] ph )
3 2 sbalv 
 |-  ( [ z / y ] A. x -. ph <-> A. x -. [ z / y ] ph )
4 1 3 xchbinx 
 |-  ( [ z / y ] -. A. x -. ph <-> -. A. x -. [ z / y ] ph )
5 df-ex 
 |-  ( E. x ph <-> -. A. x -. ph )
6 5 sbbii 
 |-  ( [ z / y ] E. x ph <-> [ z / y ] -. A. x -. ph )
7 df-ex 
 |-  ( E. x [ z / y ] ph <-> -. A. x -. [ z / y ] ph )
8 4 6 7 3bitr4i 
 |-  ( [ z / y ] E. x ph <-> E. x [ z / y ] ph )