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 ∈ A | F ⁡ x ≠ H ⁡ x
bnj1534.2 ⊢ w ∈ F → ∀ x w ∈ F
Assertion bnj1534 ⊢ D = z ∈ A | F ⁡ z ≠ H ⁡ z

Proof

Step Hyp Ref Expression
1 bnj1534.1 ⊢ D = x ∈ A | F ⁡ x ≠ H ⁡ x
2 bnj1534.2 ⊢ w ∈ F → ∀ x w ∈ F
3 nfcv ⊢ Ⅎ _ x A
4 nfcv ⊢ Ⅎ _ z A
5 nfv ⊢ Ⅎ z F ⁡ x ≠ H ⁡ x
6 2 nfcii ⊢ Ⅎ _ x F
7 nfcv ⊢ Ⅎ _ x z
8 6 7 nffv ⊢ Ⅎ _ x F ⁡ z
9 nfcv ⊢ Ⅎ _ x H ⁡ z
10 8 9 nfne ⊢ Ⅎ 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 ∈ A | F ⁡ x ≠ H ⁡ x = z ∈ A | F ⁡ z ≠ H ⁡ z
15 1 14 eqtri ⊢ D = z ∈ A | F ⁡ z ≠ H ⁡ z