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

Theorem axsepgfromrep 5192
Description: A more general version axsepg 5195 of the axiom scheme of separation ax-sep 5194 derived from the axiom scheme of replacement ax-rep 5181 (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 2117 to ax-13 2383. (Revised by SN, 25-Sep-2023.) Use ax-sep 5194 instead (or axsepg 5195 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 5188 . . 3 (∀𝑤∃*𝑥(𝑤 = 𝑥𝜑) → ∃𝑦𝑥(𝑥𝑦 ↔ ∃𝑤𝑧 (𝑤 = 𝑥𝜑)))
2 euequ 2677 . . . . 5 ∃!𝑥 𝑥 = 𝑤
32eumoi 2658 . . . 4 ∃*𝑥 𝑥 = 𝑤
4 equcomi 2017 . . . . . 6 (𝑤 = 𝑥𝑥 = 𝑤)
54adantr 483 . . . . 5 ((𝑤 = 𝑥𝜑) → 𝑥 = 𝑤)
65moimi 2621 . . . 4 (∃*𝑥 𝑥 = 𝑤 → ∃*𝑥(𝑤 = 𝑥𝜑))
73, 6ax-mp 5 . . 3 ∃*𝑥(𝑤 = 𝑥𝜑)
81, 7mpg 1791 . 2 𝑦𝑥(𝑥𝑦 ↔ ∃𝑤𝑧 (𝑤 = 𝑥𝜑))
9 df-rex 3142 . . . . . 6 (∃𝑤𝑧 (𝑤 = 𝑥𝜑) ↔ ∃𝑤(𝑤𝑧 ∧ (𝑤 = 𝑥𝜑)))
10 an12 643 . . . . . . 7 ((𝑤 = 𝑥 ∧ (𝑤𝑧𝜑)) ↔ (𝑤𝑧 ∧ (𝑤 = 𝑥𝜑)))
1110exbii 1841 . . . . . 6 (∃𝑤(𝑤 = 𝑥 ∧ (𝑤𝑧𝜑)) ↔ ∃𝑤(𝑤𝑧 ∧ (𝑤 = 𝑥𝜑)))
12 elequ1 2114 . . . . . . . 8 (𝑤 = 𝑥 → (𝑤𝑧𝑥𝑧))
1312anbi1d 631 . . . . . . 7 (𝑤 = 𝑥 → ((𝑤𝑧𝜑) ↔ (𝑥𝑧𝜑)))
1413equsexvw 2004 . . . . . 6 (∃𝑤(𝑤 = 𝑥 ∧ (𝑤𝑧𝜑)) ↔ (𝑥𝑧𝜑))
159, 11, 143bitr2i 301 . . . . 5 (∃𝑤𝑧 (𝑤 = 𝑥𝜑) ↔ (𝑥𝑧𝜑))
1615bibi2i 340 . . . 4 ((𝑥𝑦 ↔ ∃𝑤𝑧 (𝑤 = 𝑥𝜑)) ↔ (𝑥𝑦 ↔ (𝑥𝑧𝜑)))
1716albii 1813 . . 3 (∀𝑥(𝑥𝑦 ↔ ∃𝑤𝑧 (𝑤 = 𝑥𝜑)) ↔ ∀𝑥(𝑥𝑦 ↔ (𝑥𝑧𝜑)))
1817exbii 1841 . 2 (∃𝑦𝑥(𝑥𝑦 ↔ ∃𝑤𝑧 (𝑤 = 𝑥𝜑)) ↔ ∃𝑦𝑥(𝑥𝑦 ↔ (𝑥𝑧𝜑)))
198, 18mpbi 232 1 𝑦𝑥(𝑥𝑦 ↔ (𝑥𝑧𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 208  wa 398  wal 1528  wex 1773  ∃*wmo 2614  wrex 3137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-rep 5181
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1774  df-mo 2616  df-eu 2648  df-rex 3142
This theorem is referenced by:  axsep  5193
  Copyright terms: Public domain W3C validator