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

Metamath Proof Explorer

Theorem bnj1534

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1534.1 
|- D = { x e. A | ( F ` x ) =/= ( H ` x ) }
bnj1534.2 
|- ( w e. F -> A. x w e. F )
Assertion bnj1534 
|- D = { z e. A | ( F ` z ) =/= ( H ` z ) }

Proof

Step Hyp Ref Expression
1 bnj1534.1 
 |-  D = { x e. A | ( F ` x ) =/= ( H ` x ) }
2 bnj1534.2 
 |-  ( w e. F -> A. x w e. F )
3 nfcv 
 |-  F/_ x A
4 nfcv 
 |-  F/_ z A
5 nfv 
 |-  F/ z ( F ` x ) =/= ( H ` x )
6 2 nfcii 
 |-  F/_ x F
7 nfcv 
 |-  F/_ x z
8 6 7 nffv 
 |-  F/_ x ( F ` z )
9 nfcv 
 |-  F/_ x ( H ` z )
10 8 9 nfne 
 |-  F/ x ( F ` z ) =/= ( H ` z )
11 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
12 fveq2 
 |-  ( x = z -> ( H ` x ) = ( H ` z ) )
13 11 12 neeq12d 
 |-  ( x = z -> ( ( F ` x ) =/= ( H ` x ) <-> ( F ` z ) =/= ( H ` z ) ) )
14 3 4 5 10 13 cbvrabw 
 |-  { x e. A | ( F ` x ) =/= ( H ` x ) } = { z e. A | ( F ` z ) =/= ( H ` z ) }
15 1 14 eqtri 
 |-  D = { z e. A | ( F ` z ) =/= ( H ` z ) }