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 ⊢ 𝐷 = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐻 ‘ 𝑥 ) }
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 ⊢ 𝐷 = { 𝑧 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐻 ‘ 𝑧 ) }