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