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

Metamath Proof Explorer

Theorem nfsb4t

Description: A variable not free in a proposition remains so after substitution in that proposition with a distinct variable (closed form of nfsb4 ). Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 7-Apr-2004) (Revised by Mario Carneiro, 4-Oct-2016) (Proof shortened by Wolf Lammen, 11-May-2018) (New usage is discouraged.)

Ref Expression
Assertion nfsb4t 
|- ( A. x F/ z ph -> ( -. A. z z = y -> F/ z [ y / x ] ph ) )

Proof

Step Hyp Ref Expression
1 sbequ12 
 |-  ( x = y -> ( ph <-> [ y / x ] ph ) )
2 1 sps 
 |-  ( A. x x = y -> ( ph <-> [ y / x ] ph ) )
3 2 drnf2 
 |-  ( A. x x = y -> ( F/ z ph <-> F/ z [ y / x ] ph ) )
4 3 biimpd 
 |-  ( A. x x = y -> ( F/ z ph -> F/ z [ y / x ] ph ) )
5 4 spsd 
 |-  ( A. x x = y -> ( A. x F/ z ph -> F/ z [ y / x ] ph ) )
6 5 impcom 
 |-  ( ( A. x F/ z ph /\ A. x x = y ) -> F/ z [ y / x ] ph )
7 6 a1d 
 |-  ( ( A. x F/ z ph /\ A. x x = y ) -> ( -. A. z z = y -> F/ z [ y / x ] ph ) )
8 nfnf1 
 |-  F/ z F/ z ph
9 8 nfal 
 |-  F/ z A. x F/ z ph
10 nfnae 
 |-  F/ z -. A. x x = y
11 9 10 nfan 
 |-  F/ z ( A. x F/ z ph /\ -. A. x x = y )
12 nfa1 
 |-  F/ x A. x F/ z ph
13 nfnae 
 |-  F/ x -. A. x x = y
14 12 13 nfan 
 |-  F/ x ( A. x F/ z ph /\ -. A. x x = y )
15 sp 
 |-  ( A. x F/ z ph -> F/ z ph )
16 15 adantr 
 |-  ( ( A. x F/ z ph /\ -. A. x x = y ) -> F/ z ph )
17 nfsb2 
 |-  ( -. A. x x = y -> F/ x [ y / x ] ph )
18 17 adantl 
 |-  ( ( A. x F/ z ph /\ -. A. x x = y ) -> F/ x [ y / x ] ph )
19 1 a1i 
 |-  ( ( A. x F/ z ph /\ -. A. x x = y ) -> ( x = y -> ( ph <-> [ y / x ] ph ) ) )
20 11 14 16 18 19 dvelimdf 
 |-  ( ( A. x F/ z ph /\ -. A. x x = y ) -> ( -. A. z z = y -> F/ z [ y / x ] ph ) )
21 7 20 pm2.61dan 
 |-  ( A. x F/ z ph -> ( -. A. z z = y -> F/ z [ y / x ] ph ) )