Mathbox for BJ < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-axrep5 Structured version   Visualization version   GIF version

Theorem bj-axrep5 32917
 Description: Remove dependency on ax-13 2282 from axrep5 4809. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
Hypothesis
Ref Expression
bj-axrep5.1 𝑧𝜑
Assertion
Ref Expression
bj-axrep5 (∀𝑥(𝑥𝑤 → ∃𝑧𝑦(𝜑𝑦 = 𝑧)) → ∃𝑧𝑦(𝑦𝑧 ↔ ∃𝑥(𝑥𝑤𝜑)))
Distinct variable group:   𝑥,𝑦,𝑧,𝑤
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤)

Proof of Theorem bj-axrep5
StepHypRef Expression
1 19.37v 1966 . . . . 5 (∃𝑧(𝑥𝑤 → ∀𝑦(𝜑𝑦 = 𝑧)) ↔ (𝑥𝑤 → ∃𝑧𝑦(𝜑𝑦 = 𝑧)))
2 impexp 461 . . . . . . . 8 (((𝑥𝑤𝜑) → 𝑦 = 𝑧) ↔ (𝑥𝑤 → (𝜑𝑦 = 𝑧)))
32albii 1787 . . . . . . 7 (∀𝑦((𝑥𝑤𝜑) → 𝑦 = 𝑧) ↔ ∀𝑦(𝑥𝑤 → (𝜑𝑦 = 𝑧)))
4 19.21v 1908 . . . . . . 7 (∀𝑦(𝑥𝑤 → (𝜑𝑦 = 𝑧)) ↔ (𝑥𝑤 → ∀𝑦(𝜑𝑦 = 𝑧)))
53, 4bitr2i 265 . . . . . 6 ((𝑥𝑤 → ∀𝑦(𝜑𝑦 = 𝑧)) ↔ ∀𝑦((𝑥𝑤𝜑) → 𝑦 = 𝑧))
65exbii 1814 . . . . 5 (∃𝑧(𝑥𝑤 → ∀𝑦(𝜑𝑦 = 𝑧)) ↔ ∃𝑧𝑦((𝑥𝑤𝜑) → 𝑦 = 𝑧))
71, 6bitr3i 266 . . . 4 ((𝑥𝑤 → ∃𝑧𝑦(𝜑𝑦 = 𝑧)) ↔ ∃𝑧𝑦((𝑥𝑤𝜑) → 𝑦 = 𝑧))
87albii 1787 . . 3 (∀𝑥(𝑥𝑤 → ∃𝑧𝑦(𝜑𝑦 = 𝑧)) ↔ ∀𝑥𝑧𝑦((𝑥𝑤𝜑) → 𝑦 = 𝑧))
9 nfv 1883 . . . . 5 𝑧 𝑥𝑤
10 bj-axrep5.1 . . . . 5 𝑧𝜑
119, 10nfan 1868 . . . 4 𝑧(𝑥𝑤𝜑)
1211bj-axrep4 32916 . . 3 (∀𝑥𝑧𝑦((𝑥𝑤𝜑) → 𝑦 = 𝑧) → ∃𝑧𝑦(𝑦𝑧 ↔ ∃𝑥(𝑥𝑤 ∧ (𝑥𝑤𝜑))))
138, 12sylbi 207 . 2 (∀𝑥(𝑥𝑤 → ∃𝑧𝑦(𝜑𝑦 = 𝑧)) → ∃𝑧𝑦(𝑦𝑧 ↔ ∃𝑥(𝑥𝑤 ∧ (𝑥𝑤𝜑))))
14 anabs5 868 . . . . . 6 ((𝑥𝑤 ∧ (𝑥𝑤𝜑)) ↔ (𝑥𝑤𝜑))
1514exbii 1814 . . . . 5 (∃𝑥(𝑥𝑤 ∧ (𝑥𝑤𝜑)) ↔ ∃𝑥(𝑥𝑤𝜑))
1615bibi2i 326 . . . 4 ((𝑦𝑧 ↔ ∃𝑥(𝑥𝑤 ∧ (𝑥𝑤𝜑))) ↔ (𝑦𝑧 ↔ ∃𝑥(𝑥𝑤𝜑)))
1716albii 1787 . . 3 (∀𝑦(𝑦𝑧 ↔ ∃𝑥(𝑥𝑤 ∧ (𝑥𝑤𝜑))) ↔ ∀𝑦(𝑦𝑧 ↔ ∃𝑥(𝑥𝑤𝜑)))
1817exbii 1814 . 2 (∃𝑧𝑦(𝑦𝑧 ↔ ∃𝑥(𝑥𝑤 ∧ (𝑥𝑤𝜑))) ↔ ∃𝑧𝑦(𝑦𝑧 ↔ ∃𝑥(𝑥𝑤𝜑)))
1913, 18sylib 208 1 (∀𝑥(𝑥𝑤 → ∃𝑧𝑦(𝜑𝑦 = 𝑧)) → ∃𝑧𝑦(𝑦𝑧 ↔ ∃𝑥(𝑥𝑤𝜑)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383  ∀wal 1521  ∃wex 1744  Ⅎwnf 1748 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-rep 4804 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750 This theorem is referenced by:  bj-axsep  32918
 Copyright terms: Public domain W3C validator