Metamath Proof Explorer


Theorem nfabdwOLD

Description: Obsolete version of nfabdw as of 23-Sep-2024. (Contributed by Mario Carneiro, 8-Oct-2016) (Revised by Gino Giotto, 10-Jan-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses nfabdw.1
|- F/ y ph
nfabdw.2
|- ( ph -> F/ x ps )
Assertion nfabdwOLD
|- ( ph -> F/_ x { y | ps } )

Proof

Step Hyp Ref Expression
1 nfabdw.1
 |-  F/ y ph
2 nfabdw.2
 |-  ( ph -> F/ x ps )
3 nfv
 |-  F/ z ph
4 df-clab
 |-  ( z e. { y | ps } <-> [ z / y ] ps )
5 1 2 alrimi
 |-  ( ph -> A. y F/ x ps )
6 nfa1
 |-  F/ y A. y F/ x ps
7 sb6
 |-  ( [ z / y ] ps <-> A. y ( y = z -> ps ) )
8 7 a1i
 |-  ( A. y F/ x ps -> ( [ z / y ] ps <-> A. y ( y = z -> ps ) ) )
9 7 biimpri
 |-  ( A. y ( y = z -> ps ) -> [ z / y ] ps )
10 9 axc4i
 |-  ( A. y ( y = z -> ps ) -> A. y [ z / y ] ps )
11 8 10 syl6bi
 |-  ( A. y F/ x ps -> ( [ z / y ] ps -> A. y [ z / y ] ps ) )
12 6 11 nf5d
 |-  ( A. y F/ x ps -> F/ y [ z / y ] ps )
13 6 12 nfim1
 |-  F/ y ( A. y F/ x ps -> [ z / y ] ps )
14 sbequ12
 |-  ( y = z -> ( ps <-> [ z / y ] ps ) )
15 14 imbi2d
 |-  ( y = z -> ( ( A. y F/ x ps -> ps ) <-> ( A. y F/ x ps -> [ z / y ] ps ) ) )
16 13 15 equsalv
 |-  ( A. y ( y = z -> ( A. y F/ x ps -> ps ) ) <-> ( A. y F/ x ps -> [ z / y ] ps ) )
17 16 bicomi
 |-  ( ( A. y F/ x ps -> [ z / y ] ps ) <-> A. y ( y = z -> ( A. y F/ x ps -> ps ) ) )
18 nfv
 |-  F/ x y = z
19 nfnf1
 |-  F/ x F/ x ps
20 19 nfal
 |-  F/ x A. y F/ x ps
21 sp
 |-  ( A. y F/ x ps -> F/ x ps )
22 20 21 nfim1
 |-  F/ x ( A. y F/ x ps -> ps )
23 18 22 nfim
 |-  F/ x ( y = z -> ( A. y F/ x ps -> ps ) )
24 23 nfal
 |-  F/ x A. y ( y = z -> ( A. y F/ x ps -> ps ) )
25 17 24 nfxfr
 |-  F/ x ( A. y F/ x ps -> [ z / y ] ps )
26 pm5.5
 |-  ( A. y F/ x ps -> ( ( A. y F/ x ps -> [ z / y ] ps ) <-> [ z / y ] ps ) )
27 20 26 nfbidf
 |-  ( A. y F/ x ps -> ( F/ x ( A. y F/ x ps -> [ z / y ] ps ) <-> F/ x [ z / y ] ps ) )
28 25 27 mpbii
 |-  ( A. y F/ x ps -> F/ x [ z / y ] ps )
29 5 28 syl
 |-  ( ph -> F/ x [ z / y ] ps )
30 4 29 nfxfrd
 |-  ( ph -> F/ x z e. { y | ps } )
31 3 30 nfcd
 |-  ( ph -> F/_ x { y | ps } )