Metamath Proof Explorer

Theorem nfabdw

Description: Bound-variable hypothesis builder for a class abstraction. Version of nfabd with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 8-Oct-2016) (Revised by Gino Giotto, 10-Jan-2024)

Ref Expression
Hypotheses nfabdw.1 
|- F/ y ph
nfabdw.2 
|- ( ph -> F/ x ps )
Assertion nfabdw 
|- ( 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 } )