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	⊢ 𝐷 = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐻 ‘ 𝑥 ) }
	bnj1534.2	⊢ ( 𝑤 ∈ 𝐹 → ∀ 𝑥 𝑤 ∈ 𝐹 )
Assertion	bnj1534	⊢ 𝐷 = { 𝑧 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐻 ‘ 𝑧 ) }

Proof

Step	Hyp	Ref	Expression
1		bnj1534.1	⊢ 𝐷 = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐻 ‘ 𝑥 ) }
2		bnj1534.2	⊢ ( 𝑤 ∈ 𝐹 → ∀ 𝑥 𝑤 ∈ 𝐹 )
3		nfcv	⊢ Ⅎ 𝑥 𝐴
4		nfcv	⊢ Ⅎ 𝑧 𝐴
5		nfv	⊢ Ⅎ 𝑧 ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐻 ‘ 𝑥 )
6	2	nfcii	⊢ Ⅎ 𝑥 𝐹
7		nfcv	⊢ Ⅎ 𝑥 𝑧
8	6 7	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑧 )
9		nfcv	⊢ Ⅎ 𝑥 ( 𝐻 ‘ 𝑧 )
10	8 9	nfne	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐻 ‘ 𝑧 )
11		fveq2	⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
12		fveq2	⊢ ( 𝑥 = 𝑧 → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑧 ) )
13	11 12	neeq12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐻 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐻 ‘ 𝑧 ) ) )
14	3 4 5 10 13	cbvrabw	⊢ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐻 ‘ 𝑥 ) } = { 𝑧 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐻 ‘ 𝑧 ) }
15	1 14	eqtri	⊢ 𝐷 = { 𝑧 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐻 ‘ 𝑧 ) }