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 30329
 Description: Technical lemma for bnj69 30332. 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 1855 . . . . . . 7 (∀𝑤((𝜑𝜓) → (𝑧𝐵 ∧ (𝑤𝐵 → ¬ 𝑤𝑅𝑧))) ↔ ((𝜑𝜓) → ∀𝑤(𝑧𝐵 ∧ (𝑤𝐵 → ¬ 𝑤𝑅𝑧))))
32exbii 1764 . . . . . 6 (∃𝑧𝑤((𝜑𝜓) → (𝑧𝐵 ∧ (𝑤𝐵 → ¬ 𝑤𝑅𝑧))) ↔ ∃𝑧((𝜑𝜓) → ∀𝑤(𝑧𝐵 ∧ (𝑤𝐵 → ¬ 𝑤𝑅𝑧))))
41, 3mpbi 219 . . . . 5 𝑧((𝜑𝜓) → ∀𝑤(𝑧𝐵 ∧ (𝑤𝐵 → ¬ 𝑤𝑅𝑧)))
5419.37iv 1898 . . . 4 ((𝜑𝜓) → ∃𝑧𝑤(𝑧𝐵 ∧ (𝑤𝐵 → ¬ 𝑤𝑅𝑧)))
6 19.28v 1896 . . . . 5 (∀𝑤(𝑧𝐵 ∧ (𝑤𝐵 → ¬ 𝑤𝑅𝑧)) ↔ (𝑧𝐵 ∧ ∀𝑤(𝑤𝐵 → ¬ 𝑤𝑅𝑧)))
76exbii 1764 . . . 4 (∃𝑧𝑤(𝑧𝐵 ∧ (𝑤𝐵 → ¬ 𝑤𝑅𝑧)) ↔ ∃𝑧(𝑧𝐵 ∧ ∀𝑤(𝑤𝐵 → ¬ 𝑤𝑅𝑧)))
85, 7sylib 207 . . 3 ((𝜑𝜓) → ∃𝑧(𝑧𝐵 ∧ ∀𝑤(𝑤𝐵 → ¬ 𝑤𝑅𝑧)))
9 df-ral 2901 . . . . 5 (∀𝑤𝐵 ¬ 𝑤𝑅𝑧 ↔ ∀𝑤(𝑤𝐵 → ¬ 𝑤𝑅𝑧))
109anbi2i 726 . . . 4 ((𝑧𝐵 ∧ ∀𝑤𝐵 ¬ 𝑤𝑅𝑧) ↔ (𝑧𝐵 ∧ ∀𝑤(𝑤𝐵 → ¬ 𝑤𝑅𝑧)))
1110exbii 1764 . . 3 (∃𝑧(𝑧𝐵 ∧ ∀𝑤𝐵 ¬ 𝑤𝑅𝑧) ↔ ∃𝑧(𝑧𝐵 ∧ ∀𝑤(𝑤𝐵 → ¬ 𝑤𝑅𝑧)))
128, 11sylibr 223 . 2 ((𝜑𝜓) → ∃𝑧(𝑧𝐵 ∧ ∀𝑤𝐵 ¬ 𝑤𝑅𝑧))
13 df-rex 2902 . 2 (∃𝑧𝐵𝑤𝐵 ¬ 𝑤𝑅𝑧 ↔ ∃𝑧(𝑧𝐵 ∧ ∀𝑤𝐵 ¬ 𝑤𝑅𝑧))
1412, 13sylibr 223 1 ((𝜑𝜓) → ∃𝑧𝐵𝑤𝐵 ¬ 𝑤𝑅𝑧)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383  ∀wal 1473  ∃wex 1695   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897   class class class wbr 4583 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902 This theorem is referenced by:  bnj1190  30330
 Copyright terms: Public domain W3C validator