MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axrep4v Structured version   Visualization version   GIF version

Theorem axrep4v 5289
Description: Version of axrep4 5290 with a disjoint variable condition, requiring fewer axioms. (Contributed by Matthew House, 18-Sep-2025.)
Assertion
Ref Expression
axrep4v (∀𝑥𝑧𝑦(𝜑𝑦 = 𝑧) → ∃𝑧𝑦(𝑦𝑧 ↔ ∃𝑥(𝑥𝑤𝜑)))
Distinct variable groups:   𝑥,𝑤,𝑦,𝑧   𝜑,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑤)

Proof of Theorem axrep4v
StepHypRef Expression
1 ax-rep 5284 . 2 (∀𝑥𝑧𝑦(∀𝑧𝜑𝑦 = 𝑧) → ∃𝑧𝑦(𝑦𝑧 ↔ ∃𝑥(𝑥𝑤 ∧ ∀𝑧𝜑)))
2 19.3v 1978 . . . . . 6 (∀𝑧𝜑𝜑)
32imbi1i 349 . . . . 5 ((∀𝑧𝜑𝑦 = 𝑧) ↔ (𝜑𝑦 = 𝑧))
43albii 1815 . . . 4 (∀𝑦(∀𝑧𝜑𝑦 = 𝑧) ↔ ∀𝑦(𝜑𝑦 = 𝑧))
54exbii 1844 . . 3 (∃𝑧𝑦(∀𝑧𝜑𝑦 = 𝑧) ↔ ∃𝑧𝑦(𝜑𝑦 = 𝑧))
65albii 1815 . 2 (∀𝑥𝑧𝑦(∀𝑧𝜑𝑦 = 𝑧) ↔ ∀𝑥𝑧𝑦(𝜑𝑦 = 𝑧))
72anbi2i 623 . . . . . 6 ((𝑥𝑤 ∧ ∀𝑧𝜑) ↔ (𝑥𝑤𝜑))
87exbii 1844 . . . . 5 (∃𝑥(𝑥𝑤 ∧ ∀𝑧𝜑) ↔ ∃𝑥(𝑥𝑤𝜑))
98bibi2i 337 . . . 4 ((𝑦𝑧 ↔ ∃𝑥(𝑥𝑤 ∧ ∀𝑧𝜑)) ↔ (𝑦𝑧 ↔ ∃𝑥(𝑥𝑤𝜑)))
109albii 1815 . . 3 (∀𝑦(𝑦𝑧 ↔ ∃𝑥(𝑥𝑤 ∧ ∀𝑧𝜑)) ↔ ∀𝑦(𝑦𝑧 ↔ ∃𝑥(𝑥𝑤𝜑)))
1110exbii 1844 . 2 (∃𝑧𝑦(𝑦𝑧 ↔ ∃𝑥(𝑥𝑤 ∧ ∀𝑧𝜑)) ↔ ∃𝑧𝑦(𝑦𝑧 ↔ ∃𝑥(𝑥𝑤𝜑)))
121, 6, 113imtr3i 291 1 (∀𝑥𝑧𝑦(𝜑𝑦 = 𝑧) → ∃𝑧𝑦(𝑦𝑧 ↔ ∃𝑥(𝑥𝑤𝜑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1534  wex 1775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-rep 5284
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776
This theorem is referenced by:  axrep6  5293  axprlem3  5430
  Copyright terms: Public domain W3C validator