This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj1185

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

Ref Expression
Hypothesis bnj1185.1 ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ¬ 𝑤 𝑅 𝑧 )
Assertion bnj1185 ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )

Proof

Step Hyp Ref Expression
1 bnj1185.1 ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ¬ 𝑤 𝑅 𝑧 )
2 breq1 ⊢ ( 𝑤 = 𝑦 → ( 𝑤 𝑅 𝑧 ↔ 𝑦 𝑅 𝑧 ) )
3 2 notbid ⊢ ( 𝑤 = 𝑦 → ( ¬ 𝑤 𝑅 𝑧 ↔ ¬ 𝑦 𝑅 𝑧 ) )
4 3 cbvralvw ⊢ ( ∀ 𝑤 ∈ 𝐵 ¬ 𝑤 𝑅 𝑧 ↔ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑧 )
5 4 rexbii ⊢ ( ∃ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ¬ 𝑤 𝑅 𝑧 ↔ ∃ 𝑧 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑧 )
6 1 5 sylib ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑧 )
7 eleq1w ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵 ) )
8 breq2 ⊢ ( 𝑧 = 𝑥 → ( 𝑦 𝑅 𝑧 ↔ 𝑦 𝑅 𝑥 ) )
9 8 notbid ⊢ ( 𝑧 = 𝑥 → ( ¬ 𝑦 𝑅 𝑧 ↔ ¬ 𝑦 𝑅 𝑥 ) )
10 9 ralbidv ⊢ ( 𝑧 = 𝑥 → ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑧 ↔ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
11 7 10 anbi12d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑧 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) ) )
12 11 cbvexvw ⊢ ( ∃ 𝑧 ( 𝑧 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑧 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
13 df-rex ⊢ ( ∃ 𝑧 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑧 ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑧 ) )
14 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
15 12 13 14 3bitr4ri ⊢ ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ↔ ∃ 𝑧 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑧 )
16 6 15 sylibr ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )