Metamath Proof Explorer

Theorem bnj1533

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1533.1 ⊢ θ → ∀ z ∈ B ¬ z ∈ D
bnj1533.2 ⊢ B ⊆ A
bnj1533.3 ⊢ D = z ∈ A | C ≠ E
Assertion bnj1533 ⊢ θ → ∀ z ∈ B C = E

Proof

Step Hyp Ref Expression
1 bnj1533.1 ⊢ θ → ∀ z ∈ B ¬ z ∈ D
2 bnj1533.2 ⊢ B ⊆ A
3 bnj1533.3 ⊢ D = z ∈ A | C ≠ E
4 1 bnj1211 ⊢ θ → ∀ z z ∈ B → ¬ z ∈ D
5 3 reqabi ⊢ z ∈ D ↔ z ∈ A ∧ C ≠ E
6 5 notbii ⊢ ¬ z ∈ D ↔ ¬ z ∈ A ∧ C ≠ E
7 imnan ⊢ z ∈ A → ¬ C ≠ E ↔ ¬ z ∈ A ∧ C ≠ E
8 nne ⊢ ¬ C ≠ E ↔ C = E
9 8 imbi2i ⊢ z ∈ A → ¬ C ≠ E ↔ z ∈ A → C = E
10 6 7 9 3bitr2i ⊢ ¬ z ∈ D ↔ z ∈ A → C = E
11 10 imbi2i ⊢ z ∈ B → ¬ z ∈ D ↔ z ∈ B → z ∈ A → C = E
12 2 sseli ⊢ z ∈ B → z ∈ A
13 12 imim1i ⊢ z ∈ A → C = E → z ∈ B → C = E
14 ax-1 ⊢ z ∈ A → C = E → z ∈ B → z ∈ A → C = E
15 14 anim1i ⊢ z ∈ A → C = E ∧ z ∈ B → z ∈ B → z ∈ A → C = E ∧ z ∈ B
16 simpr ⊢ z ∈ B → z ∈ A → C = E ∧ z ∈ B → z ∈ B
17 simpl ⊢ z ∈ B → z ∈ A → C = E ∧ z ∈ B → z ∈ B → z ∈ A → C = E
18 16 17 mpd ⊢ z ∈ B → z ∈ A → C = E ∧ z ∈ B → z ∈ A → C = E
19 18 16 jca ⊢ z ∈ B → z ∈ A → C = E ∧ z ∈ B → z ∈ A → C = E ∧ z ∈ B
20 15 19 impbii ⊢ z ∈ A → C = E ∧ z ∈ B ↔ z ∈ B → z ∈ A → C = E ∧ z ∈ B
21 20 imbi1i ⊢ z ∈ A → C = E ∧ z ∈ B → C = E ↔ z ∈ B → z ∈ A → C = E ∧ z ∈ B → C = E
22 impexp ⊢ z ∈ A → C = E ∧ z ∈ B → C = E ↔ z ∈ A → C = E → z ∈ B → C = E
23 impexp ⊢ z ∈ B → z ∈ A → C = E ∧ z ∈ B → C = E ↔ z ∈ B → z ∈ A → C = E → z ∈ B → C = E
24 21 22 23 3bitr3i ⊢ z ∈ A → C = E → z ∈ B → C = E ↔ z ∈ B → z ∈ A → C = E → z ∈ B → C = E
25 13 24 mpbi ⊢ z ∈ B → z ∈ A → C = E → z ∈ B → C = E
26 11 25 sylbi ⊢ z ∈ B → ¬ z ∈ D → z ∈ B → C = E
27 4 26 sylg ⊢ θ → ∀ z z ∈ B → C = E
28 27 bnj1142 ⊢ θ → ∀ z ∈ B C = E