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 ) }