Metamath Proof Explorer


Theorem sbex

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

Ref Expression
Assertion sbex zyxφxzyφ

Proof

Step Hyp Ref Expression
1 sbn zy¬x¬φ¬zyx¬φ
2 sbn zy¬φ¬zyφ
3 2 sbalv zyx¬φx¬zyφ
4 1 3 xchbinx zy¬x¬φ¬x¬zyφ
5 df-ex xφ¬x¬φ
6 5 sbbii zyxφzy¬x¬φ
7 df-ex xzyφ¬x¬zyφ
8 4 6 7 3bitr4i zyxφxzyφ