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

Metamath Proof Explorer

Theorem nfabd2

Description: Bound-variable hypothesis builder for a class abstraction. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Mario Carneiro, 8-Oct-2016) (Proof shortened by Wolf Lammen, 10-May-2023) (New usage is discouraged.)

Ref Expression
Hypotheses nfabd2.1 
|- F/ y ph
nfabd2.2 
|- ( ( ph /\ -. A. x x = y ) -> F/ x ps )
Assertion nfabd2 
|- ( ph -> F/_ x { y | ps } )

Proof

Step Hyp Ref Expression
1 nfabd2.1 
 |-  F/ y ph
2 nfabd2.2 
 |-  ( ( ph /\ -. A. x x = y ) -> F/ x ps )
3 nfnae 
 |-  F/ y -. A. x x = y
4 1 3 nfan 
 |-  F/ y ( ph /\ -. A. x x = y )
5 4 2 nfabd 
 |-  ( ( ph /\ -. A. x x = y ) -> F/_ x { y | ps } )
6 5 ex 
 |-  ( ph -> ( -. A. x x = y -> F/_ x { y | ps } ) )
7 nfab1 
 |-  F/_ y { y | ps }
8 eqidd 
 |-  ( A. x x = y -> { y | ps } = { y | ps } )
9 8 drnfc1 
 |-  ( A. x x = y -> ( F/_ x { y | ps } <-> F/_ y { y | ps } ) )
10 7 9 mpbiri 
 |-  ( A. x x = y -> F/_ x { y | ps } )
11 6 10 pm2.61d2 
 |-  ( ph -> F/_ x { y | ps } )