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

Metamath Proof Explorer

Theorem nfopabd

Description: Bound-variable hypothesis builder for class abstraction. Deduction form. (Contributed by Scott Fenton, 26-Oct-2024)

Ref Expression
Hypotheses nfopabd.1 
|- F/ x ph
nfopabd.2 
|- F/ y ph
nfopabd.4 
|- ( ph -> F/ z ps )
Assertion nfopabd 
|- ( ph -> F/_ z { <. x , y >. | ps } )

Proof

Step Hyp Ref Expression
1 nfopabd.1 
 |-  F/ x ph
2 nfopabd.2 
 |-  F/ y ph
3 nfopabd.4 
 |-  ( ph -> F/ z ps )
4 df-opab 
 |-  { <. x , y >. | ps } = { w | E. x E. y ( w = <. x , y >. /\ ps ) }
5 nfv 
 |-  F/ w ph
6 nfvd 
 |-  ( ph -> F/ z w = <. x , y >. )
7 6 3 nfand 
 |-  ( ph -> F/ z ( w = <. x , y >. /\ ps ) )
8 2 7 nfexd 
 |-  ( ph -> F/ z E. y ( w = <. x , y >. /\ ps ) )
9 1 8 nfexd 
 |-  ( ph -> F/ z E. x E. y ( w = <. x , y >. /\ ps ) )
10 5 9 nfabdw 
 |-  ( ph -> F/_ z { w | E. x E. y ( w = <. x , y >. /\ ps ) } )
11 4 10 nfcxfrd 
 |-  ( ph -> F/_ z { <. x , y >. | ps } )