Users' Mathboxes Mathbox for Jonathan Ben-Naim < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj1186 Structured version   Visualization version   GIF version

Theorem bnj1186 32393
Description: Technical lemma for bnj69 32396. 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.)
Hypothesis
Ref Expression
bnj1186.1 𝑧𝑤((𝜑𝜓) → (𝑧𝐵 ∧ (𝑤𝐵 → ¬ 𝑤𝑅𝑧)))
Assertion
Ref Expression
bnj1186 ((𝜑𝜓) → ∃𝑧𝐵𝑤𝐵 ¬ 𝑤𝑅𝑧)
Distinct variable groups:   𝑤,𝐵   𝜑,𝑤,𝑧   𝜓,𝑤,𝑧
Allowed substitution hints:   𝐵(𝑧)   𝑅(𝑧,𝑤)

Proof of Theorem bnj1186
StepHypRef Expression
1 bnj1186.1 . . . . . 6 𝑧𝑤((𝜑𝜓) → (𝑧𝐵 ∧ (𝑤𝐵 → ¬ 𝑤𝑅𝑧)))
2 19.21v 1940 . . . . . . 7 (∀𝑤((𝜑𝜓) → (𝑧𝐵 ∧ (𝑤𝐵 → ¬ 𝑤𝑅𝑧))) ↔ ((𝜑𝜓) → ∀𝑤(𝑧𝐵 ∧ (𝑤𝐵 → ¬ 𝑤𝑅𝑧))))
32exbii 1849 . . . . . 6 (∃𝑧𝑤((𝜑𝜓) → (𝑧𝐵 ∧ (𝑤𝐵 → ¬ 𝑤𝑅𝑧))) ↔ ∃𝑧((𝜑𝜓) → ∀𝑤(𝑧𝐵 ∧ (𝑤𝐵 → ¬ 𝑤𝑅𝑧))))
41, 3mpbi 233 . . . . 5 𝑧((𝜑𝜓) → ∀𝑤(𝑧𝐵 ∧ (𝑤𝐵 → ¬ 𝑤𝑅𝑧)))
5419.37iv 1949 . . . 4 ((𝜑𝜓) → ∃𝑧𝑤(𝑧𝐵 ∧ (𝑤𝐵 → ¬ 𝑤𝑅𝑧)))
6 19.28v 1997 . . . . 5 (∀𝑤(𝑧𝐵 ∧ (𝑤𝐵 → ¬ 𝑤𝑅𝑧)) ↔ (𝑧𝐵 ∧ ∀𝑤(𝑤𝐵 → ¬ 𝑤𝑅𝑧)))
76exbii 1849 . . . 4 (∃𝑧𝑤(𝑧𝐵 ∧ (𝑤𝐵 → ¬ 𝑤𝑅𝑧)) ↔ ∃𝑧(𝑧𝐵 ∧ ∀𝑤(𝑤𝐵 → ¬ 𝑤𝑅𝑧)))
85, 7sylib 221 . . 3 ((𝜑𝜓) → ∃𝑧(𝑧𝐵 ∧ ∀𝑤(𝑤𝐵 → ¬ 𝑤𝑅𝑧)))
9 df-ral 3114 . . . . 5 (∀𝑤𝐵 ¬ 𝑤𝑅𝑧 ↔ ∀𝑤(𝑤𝐵 → ¬ 𝑤𝑅𝑧))
109anbi2i 625 . . . 4 ((𝑧𝐵 ∧ ∀𝑤𝐵 ¬ 𝑤𝑅𝑧) ↔ (𝑧𝐵 ∧ ∀𝑤(𝑤𝐵 → ¬ 𝑤𝑅𝑧)))
1110exbii 1849 . . 3 (∃𝑧(𝑧𝐵 ∧ ∀𝑤𝐵 ¬ 𝑤𝑅𝑧) ↔ ∃𝑧(𝑧𝐵 ∧ ∀𝑤(𝑤𝐵 → ¬ 𝑤𝑅𝑧)))
128, 11sylibr 237 . 2 ((𝜑𝜓) → ∃𝑧(𝑧𝐵 ∧ ∀𝑤𝐵 ¬ 𝑤𝑅𝑧))
13 df-rex 3115 . 2 (∃𝑧𝐵𝑤𝐵 ¬ 𝑤𝑅𝑧 ↔ ∃𝑧(𝑧𝐵 ∧ ∀𝑤𝐵 ¬ 𝑤𝑅𝑧))
1412, 13sylibr 237 1 ((𝜑𝜓) → ∃𝑧𝐵𝑤𝐵 ¬ 𝑤𝑅𝑧)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  wal 1536  wex 1781  wcel 2112  wral 3109  wrex 3110   class class class wbr 5033
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3114  df-rex 3115
This theorem is referenced by:  bnj1190  32394
  Copyright terms: Public domain W3C validator