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

Theorem zfrep6 7978
Description: A version of the Axiom of Replacement. Normally 𝜑 would have free variables 𝑥 and 𝑦. Axiom 6 of [Kunen] p. 12. The Separation Scheme ax-sep 5302 cannot be derived from this version and must be stated as a separate axiom in an axiom system (such as Kunen's) that uses this version in place of our ax-rep 5285. (Contributed by NM, 10-Oct-2003.)
Assertion
Ref Expression
zfrep6 (∀𝑥𝑧 ∃!𝑦𝜑 → ∃𝑤𝑥𝑧𝑦𝑤 𝜑)
Distinct variable groups:   𝜑,𝑤   𝑥,𝑦,𝑧,𝑤
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)

Proof of Theorem zfrep6
StepHypRef Expression
1 19.42v 1951 . . . . . . 7 (∃𝑦(𝑥𝑧𝜑) ↔ (𝑥𝑧 ∧ ∃𝑦𝜑))
21abbii 2807 . . . . . 6 {𝑥 ∣ ∃𝑦(𝑥𝑧𝜑)} = {𝑥 ∣ (𝑥𝑧 ∧ ∃𝑦𝜑)}
3 dmopab 5929 . . . . . 6 dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} = {𝑥 ∣ ∃𝑦(𝑥𝑧𝜑)}
4 df-rab 3434 . . . . . 6 {𝑥𝑧 ∣ ∃𝑦𝜑} = {𝑥 ∣ (𝑥𝑧 ∧ ∃𝑦𝜑)}
52, 3, 43eqtr4i 2773 . . . . 5 dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} = {𝑥𝑧 ∣ ∃𝑦𝜑}
6 euex 2575 . . . . . . 7 (∃!𝑦𝜑 → ∃𝑦𝜑)
76ralimi 3081 . . . . . 6 (∀𝑥𝑧 ∃!𝑦𝜑 → ∀𝑥𝑧𝑦𝜑)
8 rabid2 3468 . . . . . 6 (𝑧 = {𝑥𝑧 ∣ ∃𝑦𝜑} ↔ ∀𝑥𝑧𝑦𝜑)
97, 8sylibr 234 . . . . 5 (∀𝑥𝑧 ∃!𝑦𝜑𝑧 = {𝑥𝑧 ∣ ∃𝑦𝜑})
105, 9eqtr4id 2794 . . . 4 (∀𝑥𝑧 ∃!𝑦𝜑 → dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} = 𝑧)
11 vex 3482 . . . 4 𝑧 ∈ V
1210, 11eqeltrdi 2847 . . 3 (∀𝑥𝑧 ∃!𝑦𝜑 → dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∈ V)
13 eumo 2576 . . . . . . 7 (∃!𝑦𝜑 → ∃*𝑦𝜑)
1413imim2i 16 . . . . . 6 ((𝑥𝑧 → ∃!𝑦𝜑) → (𝑥𝑧 → ∃*𝑦𝜑))
15 moanimv 2617 . . . . . 6 (∃*𝑦(𝑥𝑧𝜑) ↔ (𝑥𝑧 → ∃*𝑦𝜑))
1614, 15sylibr 234 . . . . 5 ((𝑥𝑧 → ∃!𝑦𝜑) → ∃*𝑦(𝑥𝑧𝜑))
1716alimi 1808 . . . 4 (∀𝑥(𝑥𝑧 → ∃!𝑦𝜑) → ∀𝑥∃*𝑦(𝑥𝑧𝜑))
18 df-ral 3060 . . . 4 (∀𝑥𝑧 ∃!𝑦𝜑 ↔ ∀𝑥(𝑥𝑧 → ∃!𝑦𝜑))
19 funopab 6603 . . . 4 (Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ↔ ∀𝑥∃*𝑦(𝑥𝑧𝜑))
2017, 18, 193imtr4i 292 . . 3 (∀𝑥𝑧 ∃!𝑦𝜑 → Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)})
21 funrnex 7977 . . 3 (dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∈ V → (Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} → ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∈ V))
2212, 20, 21sylc 65 . 2 (∀𝑥𝑧 ∃!𝑦𝜑 → ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∈ V)
23 nfra1 3282 . . 3 𝑥𝑥𝑧 ∃!𝑦𝜑
2410eleq2d 2825 . . . 4 (∀𝑥𝑧 ∃!𝑦𝜑 → (𝑥 ∈ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ↔ 𝑥𝑧))
25 opabidw 5534 . . . . . . . . 9 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ↔ (𝑥𝑧𝜑))
26 vex 3482 . . . . . . . . . 10 𝑥 ∈ V
27 vex 3482 . . . . . . . . . 10 𝑦 ∈ V
2826, 27opelrn 5957 . . . . . . . . 9 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} → 𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)})
2925, 28sylbir 235 . . . . . . . 8 ((𝑥𝑧𝜑) → 𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)})
3029ex 412 . . . . . . 7 (𝑥𝑧 → (𝜑𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}))
3130impac 552 . . . . . 6 ((𝑥𝑧𝜑) → (𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∧ 𝜑))
3231eximi 1832 . . . . 5 (∃𝑦(𝑥𝑧𝜑) → ∃𝑦(𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∧ 𝜑))
333eqabri 2883 . . . . 5 (𝑥 ∈ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ↔ ∃𝑦(𝑥𝑧𝜑))
34 df-rex 3069 . . . . 5 (∃𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑 ↔ ∃𝑦(𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∧ 𝜑))
3532, 33, 343imtr4i 292 . . . 4 (𝑥 ∈ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} → ∃𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑)
3624, 35biimtrrdi 254 . . 3 (∀𝑥𝑧 ∃!𝑦𝜑 → (𝑥𝑧 → ∃𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑))
3723, 36ralrimi 3255 . 2 (∀𝑥𝑧 ∃!𝑦𝜑 → ∀𝑥𝑧𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑)
38 nfopab1 5218 . . . . 5 𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}
3938nfrn 5966 . . . 4 𝑥ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}
4039nfeq2 2921 . . 3 𝑥 𝑤 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}
41 nfcv 2903 . . . 4 𝑦𝑤
42 nfopab2 5219 . . . . 5 𝑦{⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}
4342nfrn 5966 . . . 4 𝑦ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}
4441, 43rexeqf 3352 . . 3 (𝑤 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} → (∃𝑦𝑤 𝜑 ↔ ∃𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑))
4540, 44ralbid 3271 . 2 (𝑤 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} → (∀𝑥𝑧𝑦𝑤 𝜑 ↔ ∀𝑥𝑧𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑))
4622, 37, 45spcedv 3598 1 (∀𝑥𝑧 ∃!𝑦𝜑 → ∃𝑤𝑥𝑧𝑦𝑤 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wal 1535   = wceq 1537  wex 1776  wcel 2106  ∃*wmo 2536  ∃!weu 2566  {cab 2712  wral 3059  wrex 3068  {crab 3433  Vcvv 3478  cop 4637  {copab 5210  dom cdm 5689  ran crn 5690  Fun wfun 6557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571
This theorem is referenced by:  bnj865  34916
  Copyright terms: Public domain W3C validator