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

Theorem axsepgfromrep 5297
Description: A more general version axsepg 5300 of the axiom scheme of separation ax-sep 5299 derived from the axiom scheme of replacement ax-rep 5285 (and first-order logic). The extra generality consists in the absence of a disjoint variable condition on 𝑧, 𝜑 (that is, variable 𝑧 may occur in formula 𝜑). See linked statements for more information. (Contributed by NM, 11-Sep-2006.) Remove dependencies on ax-9 2115 to ax-13 2370. (Revised by SN, 25-Sep-2023.) Use ax-sep 5299 instead (or axsepg 5300 if the extra generality is needed). (New usage is discouraged.)
Assertion
Ref Expression
axsepgfromrep 𝑦𝑥(𝑥𝑦 ↔ (𝑥𝑧𝜑))
Distinct variable groups:   𝑥,𝑦,𝑧   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑧)

Proof of Theorem axsepgfromrep
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 axrep6 5292 . . 3 (∀𝑤∃*𝑥(𝑤 = 𝑥𝜑) → ∃𝑦𝑥(𝑥𝑦 ↔ ∃𝑤𝑧 (𝑤 = 𝑥𝜑)))
2 euequ 2590 . . . . 5 ∃!𝑥 𝑥 = 𝑤
32eumoi 2572 . . . 4 ∃*𝑥 𝑥 = 𝑤
4 equcomi 2019 . . . . . 6 (𝑤 = 𝑥𝑥 = 𝑤)
54adantr 480 . . . . 5 ((𝑤 = 𝑥𝜑) → 𝑥 = 𝑤)
65moimi 2538 . . . 4 (∃*𝑥 𝑥 = 𝑤 → ∃*𝑥(𝑤 = 𝑥𝜑))
73, 6ax-mp 5 . . 3 ∃*𝑥(𝑤 = 𝑥𝜑)
81, 7mpg 1798 . 2 𝑦𝑥(𝑥𝑦 ↔ ∃𝑤𝑧 (𝑤 = 𝑥𝜑))
9 df-rex 3070 . . . . . 6 (∃𝑤𝑧 (𝑤 = 𝑥𝜑) ↔ ∃𝑤(𝑤𝑧 ∧ (𝑤 = 𝑥𝜑)))
10 an12 642 . . . . . . 7 ((𝑤 = 𝑥 ∧ (𝑤𝑧𝜑)) ↔ (𝑤𝑧 ∧ (𝑤 = 𝑥𝜑)))
1110exbii 1849 . . . . . 6 (∃𝑤(𝑤 = 𝑥 ∧ (𝑤𝑧𝜑)) ↔ ∃𝑤(𝑤𝑧 ∧ (𝑤 = 𝑥𝜑)))
12 elequ1 2112 . . . . . . . 8 (𝑤 = 𝑥 → (𝑤𝑧𝑥𝑧))
1312anbi1d 629 . . . . . . 7 (𝑤 = 𝑥 → ((𝑤𝑧𝜑) ↔ (𝑥𝑧𝜑)))
1413equsexvw 2007 . . . . . 6 (∃𝑤(𝑤 = 𝑥 ∧ (𝑤𝑧𝜑)) ↔ (𝑥𝑧𝜑))
159, 11, 143bitr2i 299 . . . . 5 (∃𝑤𝑧 (𝑤 = 𝑥𝜑) ↔ (𝑥𝑧𝜑))
1615bibi2i 337 . . . 4 ((𝑥𝑦 ↔ ∃𝑤𝑧 (𝑤 = 𝑥𝜑)) ↔ (𝑥𝑦 ↔ (𝑥𝑧𝜑)))
1716albii 1820 . . 3 (∀𝑥(𝑥𝑦 ↔ ∃𝑤𝑧 (𝑤 = 𝑥𝜑)) ↔ ∀𝑥(𝑥𝑦 ↔ (𝑥𝑧𝜑)))
1817exbii 1849 . 2 (∃𝑦𝑥(𝑥𝑦 ↔ ∃𝑤𝑧 (𝑤 = 𝑥𝜑)) ↔ ∃𝑦𝑥(𝑥𝑦 ↔ (𝑥𝑧𝜑)))
198, 18mpbi 229 1 𝑦𝑥(𝑥𝑦 ↔ (𝑥𝑧𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 395  wal 1538  wex 1780  ∃*wmo 2531  wrex 3069
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-rep 5285
This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-mo 2533  df-eu 2562  df-rex 3070
This theorem is referenced by:  axsep  5298
  Copyright terms: Public domain W3C validator