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

Theorem zfrep6 7088
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 4746 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 4736. (Contributed by NM, 10-Oct-2003.)
Assertion
Ref Expression
zfrep6 (∀𝑥𝑧 ∃!𝑦𝜑 → ∃𝑤𝑥𝑧𝑦𝑤 𝜑)
Distinct variable groups:   𝜑,𝑤   𝑥,𝑦,𝑧,𝑤
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)

Proof of Theorem zfrep6
StepHypRef Expression
1 euex 2493 . . . . . . 7 (∃!𝑦𝜑 → ∃𝑦𝜑)
21ralimi 2947 . . . . . 6 (∀𝑥𝑧 ∃!𝑦𝜑 → ∀𝑥𝑧𝑦𝜑)
3 rabid2 3110 . . . . . 6 (𝑧 = {𝑥𝑧 ∣ ∃𝑦𝜑} ↔ ∀𝑥𝑧𝑦𝜑)
42, 3sylibr 224 . . . . 5 (∀𝑥𝑧 ∃!𝑦𝜑𝑧 = {𝑥𝑧 ∣ ∃𝑦𝜑})
5 19.42v 1915 . . . . . . 7 (∃𝑦(𝑥𝑧𝜑) ↔ (𝑥𝑧 ∧ ∃𝑦𝜑))
65abbii 2736 . . . . . 6 {𝑥 ∣ ∃𝑦(𝑥𝑧𝜑)} = {𝑥 ∣ (𝑥𝑧 ∧ ∃𝑦𝜑)}
7 dmopab 5300 . . . . . 6 dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} = {𝑥 ∣ ∃𝑦(𝑥𝑧𝜑)}
8 df-rab 2916 . . . . . 6 {𝑥𝑧 ∣ ∃𝑦𝜑} = {𝑥 ∣ (𝑥𝑧 ∧ ∃𝑦𝜑)}
96, 7, 83eqtr4i 2653 . . . . 5 dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} = {𝑥𝑧 ∣ ∃𝑦𝜑}
104, 9syl6reqr 2674 . . . 4 (∀𝑥𝑧 ∃!𝑦𝜑 → dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} = 𝑧)
11 vex 3192 . . . 4 𝑧 ∈ V
1210, 11syl6eqel 2706 . . 3 (∀𝑥𝑧 ∃!𝑦𝜑 → dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∈ V)
13 eumo 2498 . . . . . . 7 (∃!𝑦𝜑 → ∃*𝑦𝜑)
1413imim2i 16 . . . . . 6 ((𝑥𝑧 → ∃!𝑦𝜑) → (𝑥𝑧 → ∃*𝑦𝜑))
15 moanimv 2530 . . . . . 6 (∃*𝑦(𝑥𝑧𝜑) ↔ (𝑥𝑧 → ∃*𝑦𝜑))
1614, 15sylibr 224 . . . . 5 ((𝑥𝑧 → ∃!𝑦𝜑) → ∃*𝑦(𝑥𝑧𝜑))
1716alimi 1736 . . . 4 (∀𝑥(𝑥𝑧 → ∃!𝑦𝜑) → ∀𝑥∃*𝑦(𝑥𝑧𝜑))
18 df-ral 2912 . . . 4 (∀𝑥𝑧 ∃!𝑦𝜑 ↔ ∀𝑥(𝑥𝑧 → ∃!𝑦𝜑))
19 funopab 5886 . . . 4 (Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ↔ ∀𝑥∃*𝑦(𝑥𝑧𝜑))
2017, 18, 193imtr4i 281 . . 3 (∀𝑥𝑧 ∃!𝑦𝜑 → Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)})
21 funrnex 7087 . . 3 (dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∈ V → (Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} → ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∈ V))
2212, 20, 21sylc 65 . 2 (∀𝑥𝑧 ∃!𝑦𝜑 → ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∈ V)
23 nfra1 2936 . . 3 𝑥𝑥𝑧 ∃!𝑦𝜑
2410eleq2d 2684 . . . 4 (∀𝑥𝑧 ∃!𝑦𝜑 → (𝑥 ∈ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ↔ 𝑥𝑧))
25 opabid 4947 . . . . . . . . 9 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ↔ (𝑥𝑧𝜑))
26 vex 3192 . . . . . . . . . 10 𝑥 ∈ V
27 vex 3192 . . . . . . . . . 10 𝑦 ∈ V
2826, 27opelrn 5322 . . . . . . . . 9 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} → 𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)})
2925, 28sylbir 225 . . . . . . . 8 ((𝑥𝑧𝜑) → 𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)})
3029ex 450 . . . . . . 7 (𝑥𝑧 → (𝜑𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}))
3130impac 650 . . . . . 6 ((𝑥𝑧𝜑) → (𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∧ 𝜑))
3231eximi 1759 . . . . 5 (∃𝑦(𝑥𝑧𝜑) → ∃𝑦(𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∧ 𝜑))
337abeq2i 2732 . . . . 5 (𝑥 ∈ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ↔ ∃𝑦(𝑥𝑧𝜑))
34 df-rex 2913 . . . . 5 (∃𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑 ↔ ∃𝑦(𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∧ 𝜑))
3532, 33, 343imtr4i 281 . . . 4 (𝑥 ∈ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} → ∃𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑)
3624, 35syl6bir 244 . . 3 (∀𝑥𝑧 ∃!𝑦𝜑 → (𝑥𝑧 → ∃𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑))
3723, 36ralrimi 2952 . 2 (∀𝑥𝑧 ∃!𝑦𝜑 → ∀𝑥𝑧𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑)
38 nfopab1 4686 . . . . . 6 𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}
3938nfrn 5333 . . . . 5 𝑥ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}
4039nfeq2 2776 . . . 4 𝑥 𝑤 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}
41 nfcv 2761 . . . . 5 𝑦𝑤
42 nfopab2 4687 . . . . . 6 𝑦{⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}
4342nfrn 5333 . . . . 5 𝑦ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}
4441, 43rexeqf 3127 . . . 4 (𝑤 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} → (∃𝑦𝑤 𝜑 ↔ ∃𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑))
4540, 44ralbid 2978 . . 3 (𝑤 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} → (∀𝑥𝑧𝑦𝑤 𝜑 ↔ ∀𝑥𝑧𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑))
4645spcegv 3283 . 2 (ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∈ V → (∀𝑥𝑧𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑 → ∃𝑤𝑥𝑧𝑦𝑤 𝜑))
4722, 37, 46sylc 65 1 (∀𝑥𝑧 ∃!𝑦𝜑 → ∃𝑤𝑥𝑧𝑦𝑤 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wal 1478   = wceq 1480  wex 1701  wcel 1987  ∃!weu 2469  ∃*wmo 2470  {cab 2607  wral 2907  wrex 2908  {crab 2911  Vcvv 3189  cop 4159  {copab 4677  dom cdm 5079  ran crn 5080  Fun wfun 5846
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860
This theorem is referenced by:  bnj865  30728
  Copyright terms: Public domain W3C validator