Metamath Proof Explorer

Theorem bnj1186

Description: Technical lemma for bnj69 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypothesis bnj1186.1 ⊢∃z∀wφ∧ψ→z∈B∧w∈B→¬wRz
Assertion bnj1186 ⊢φ∧ψ→∃z∈B∀w∈B¬wRz

Proof

Step Hyp Ref Expression
1 bnj1186.1 ⊢∃z∀wφ∧ψ→z∈B∧w∈B→¬wRz
2 19.21v ⊢∀wφ∧ψ→z∈B∧w∈B→¬wRz↔φ∧ψ→∀wz∈B∧w∈B→¬wRz
3 2 exbii ⊢∃z∀wφ∧ψ→z∈B∧w∈B→¬wRz↔∃zφ∧ψ→∀wz∈B∧w∈B→¬wRz
4 1 3 mpbi ⊢∃zφ∧ψ→∀wz∈B∧w∈B→¬wRz
5 4 19.37iv ⊢φ∧ψ→∃z∀wz∈B∧w∈B→¬wRz
6 19.28v ⊢∀wz∈B∧w∈B→¬wRz↔z∈B∧∀ww∈B→¬wRz
7 6 exbii ⊢∃z∀wz∈B∧w∈B→¬wRz↔∃zz∈B∧∀ww∈B→¬wRz
8 5 7 sylib ⊢φ∧ψ→∃zz∈B∧∀ww∈B→¬wRz
9 df-ral ⊢∀w∈B¬wRz↔∀ww∈B→¬wRz
10 9 anbi2i ⊢z∈B∧∀w∈B¬wRz↔z∈B∧∀ww∈B→¬wRz
11 10 exbii ⊢∃zz∈B∧∀w∈B¬wRz↔∃zz∈B∧∀ww∈B→¬wRz
12 8 11 sylibr ⊢φ∧ψ→∃zz∈B∧∀w∈B¬wRz
13 df-rex ⊢∃z∈B∀w∈B¬wRz↔∃zz∈B∧∀w∈B¬wRz
14 12 13 sylibr ⊢φ∧ψ→∃z∈B∀w∈B¬wRz