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 ⊢ ( 𝜃 → ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 ∈ 𝐷 )
bnj1533.2 ⊢ 𝐵 ⊆ 𝐴
bnj1533.3 ⊢ 𝐷 = { 𝑧 ∈ 𝐴 ∣ 𝐶 ≠ 𝐸 }
Assertion bnj1533 ( 𝜃 → ∀ 𝑧 ∈ 𝐵 𝐶 = 𝐸 )

Proof

Step Hyp Ref Expression
1 bnj1533.1 ⊢ ( 𝜃 → ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 ∈ 𝐷 )
2 bnj1533.2 ⊢ 𝐵 ⊆ 𝐴
3 bnj1533.3 ⊢ 𝐷 = { 𝑧 ∈ 𝐴 ∣ 𝐶 ≠ 𝐸 }
4 1 bnj1211 ⊢ ( 𝜃 → ∀ 𝑧 ( 𝑧 ∈ 𝐵 → ¬ 𝑧 ∈ 𝐷 ) )
5 3 rabeq2i ⊢ ( 𝑧 ∈ 𝐷 ↔ ( 𝑧 ∈ 𝐴 ∧ 𝐶 ≠ 𝐸 ) )
6 5 notbii ⊢ ( ¬ 𝑧 ∈ 𝐷 ↔ ¬ ( 𝑧 ∈ 𝐴 ∧ 𝐶 ≠ 𝐸 ) )
7 imnan ⊢ ( ( 𝑧 ∈ 𝐴 → ¬ 𝐶 ≠ 𝐸 ) ↔ ¬ ( 𝑧 ∈ 𝐴 ∧ 𝐶 ≠ 𝐸 ) )
8 nne ⊢ ( ¬ 𝐶 ≠ 𝐸 ↔ 𝐶 = 𝐸 )
9 8 imbi2i ⊢ ( ( 𝑧 ∈ 𝐴 → ¬ 𝐶 ≠ 𝐸 ) ↔ ( 𝑧 ∈ 𝐴 → 𝐶 = 𝐸 ) )
10 6 7 9 3bitr2i ⊢ ( ¬ 𝑧 ∈ 𝐷 ↔ ( 𝑧 ∈ 𝐴 → 𝐶 = 𝐸 ) )
11 10 imbi2i ⊢ ( ( 𝑧 ∈ 𝐵 → ¬ 𝑧 ∈ 𝐷 ) ↔ ( 𝑧 ∈ 𝐵 → ( 𝑧 ∈ 𝐴 → 𝐶 = 𝐸 ) ) )
12 2 sseli ⊢ ( 𝑧 ∈ 𝐵 → 𝑧 ∈ 𝐴 )
13 12 imim1i ⊢ ( ( 𝑧 ∈ 𝐴 → 𝐶 = 𝐸 ) → ( 𝑧 ∈ 𝐵 → 𝐶 = 𝐸 ) )
14 ax-1 ⊢ ( ( 𝑧 ∈ 𝐴 → 𝐶 = 𝐸 ) → ( 𝑧 ∈ 𝐵 → ( 𝑧 ∈ 𝐴 → 𝐶 = 𝐸 ) ) )
15 14 anim1i ⊢ ( ( ( 𝑧 ∈ 𝐴 → 𝐶 = 𝐸 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑧 ∈ 𝐵 → ( 𝑧 ∈ 𝐴 → 𝐶 = 𝐸 ) ) ∧ 𝑧 ∈ 𝐵 ) )
16 simpr ⊢ ( ( ( 𝑧 ∈ 𝐵 → ( 𝑧 ∈ 𝐴 → 𝐶 = 𝐸 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
17 simpl ⊢ ( ( ( 𝑧 ∈ 𝐵 → ( 𝑧 ∈ 𝐴 → 𝐶 = 𝐸 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 ∈ 𝐵 → ( 𝑧 ∈ 𝐴 → 𝐶 = 𝐸 ) ) )
18 16 17 mpd ⊢ ( ( ( 𝑧 ∈ 𝐵 → ( 𝑧 ∈ 𝐴 → 𝐶 = 𝐸 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 ∈ 𝐴 → 𝐶 = 𝐸 ) )
19 18 16 jca ⊢ ( ( ( 𝑧 ∈ 𝐵 → ( 𝑧 ∈ 𝐴 → 𝐶 = 𝐸 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑧 ∈ 𝐴 → 𝐶 = 𝐸 ) ∧ 𝑧 ∈ 𝐵 ) )
20 15 19 impbii ⊢ ( ( ( 𝑧 ∈ 𝐴 → 𝐶 = 𝐸 ) ∧ 𝑧 ∈ 𝐵 ) ↔ ( ( 𝑧 ∈ 𝐵 → ( 𝑧 ∈ 𝐴 → 𝐶 = 𝐸 ) ) ∧ 𝑧 ∈ 𝐵 ) )
21 20 imbi1i ⊢ ( ( ( ( 𝑧 ∈ 𝐴 → 𝐶 = 𝐸 ) ∧ 𝑧 ∈ 𝐵 ) → 𝐶 = 𝐸 ) ↔ ( ( ( 𝑧 ∈ 𝐵 → ( 𝑧 ∈ 𝐴 → 𝐶 = 𝐸 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝐶 = 𝐸 ) )
22 impexp ⊢ ( ( ( ( 𝑧 ∈ 𝐴 → 𝐶 = 𝐸 ) ∧ 𝑧 ∈ 𝐵 ) → 𝐶 = 𝐸 ) ↔ ( ( 𝑧 ∈ 𝐴 → 𝐶 = 𝐸 ) → ( 𝑧 ∈ 𝐵 → 𝐶 = 𝐸 ) ) )
23 impexp ⊢ ( ( ( ( 𝑧 ∈ 𝐵 → ( 𝑧 ∈ 𝐴 → 𝐶 = 𝐸 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝐶 = 𝐸 ) ↔ ( ( 𝑧 ∈ 𝐵 → ( 𝑧 ∈ 𝐴 → 𝐶 = 𝐸 ) ) → ( 𝑧 ∈ 𝐵 → 𝐶 = 𝐸 ) ) )
24 21 22 23 3bitr3i ⊢ ( ( ( 𝑧 ∈ 𝐴 → 𝐶 = 𝐸 ) → ( 𝑧 ∈ 𝐵 → 𝐶 = 𝐸 ) ) ↔ ( ( 𝑧 ∈ 𝐵 → ( 𝑧 ∈ 𝐴 → 𝐶 = 𝐸 ) ) → ( 𝑧 ∈ 𝐵 → 𝐶 = 𝐸 ) ) )
25 13 24 mpbi ⊢ ( ( 𝑧 ∈ 𝐵 → ( 𝑧 ∈ 𝐴 → 𝐶 = 𝐸 ) ) → ( 𝑧 ∈ 𝐵 → 𝐶 = 𝐸 ) )
26 11 25 sylbi ⊢ ( ( 𝑧 ∈ 𝐵 → ¬ 𝑧 ∈ 𝐷 ) → ( 𝑧 ∈ 𝐵 → 𝐶 = 𝐸 ) )
27 4 26 sylg ⊢ ( 𝜃 → ∀ 𝑧 ( 𝑧 ∈ 𝐵 → 𝐶 = 𝐸 ) )
28 27 bnj1142 ⊢ ( 𝜃 → ∀ 𝑧 ∈ 𝐵 𝐶 = 𝐸 )