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	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )