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

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

Proof of Theorem zfrep6
StepHypRef Expression
1 euex 2522 . . . . . . 7 (∃!𝑦𝜑 → ∃𝑦𝜑)
21ralimi 2981 . . . . . 6 (∀𝑥𝑧 ∃!𝑦𝜑 → ∀𝑥𝑧𝑦𝜑)
3 rabid2 3148 . . . . . 6 (𝑧 = {𝑥𝑧 ∣ ∃𝑦𝜑} ↔ ∀𝑥𝑧𝑦𝜑)
42, 3sylibr 224 . . . . 5 (∀𝑥𝑧 ∃!𝑦𝜑𝑧 = {𝑥𝑧 ∣ ∃𝑦𝜑})
5 19.42v 1921 . . . . . . 7 (∃𝑦(𝑥𝑧𝜑) ↔ (𝑥𝑧 ∧ ∃𝑦𝜑))
65abbii 2768 . . . . . 6 {𝑥 ∣ ∃𝑦(𝑥𝑧𝜑)} = {𝑥 ∣ (𝑥𝑧 ∧ ∃𝑦𝜑)}
7 dmopab 5367 . . . . . 6 dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} = {𝑥 ∣ ∃𝑦(𝑥𝑧𝜑)}
8 df-rab 2950 . . . . . 6 {𝑥𝑧 ∣ ∃𝑦𝜑} = {𝑥 ∣ (𝑥𝑧 ∧ ∃𝑦𝜑)}
96, 7, 83eqtr4i 2683 . . . . 5 dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} = {𝑥𝑧 ∣ ∃𝑦𝜑}
104, 9syl6reqr 2704 . . . 4 (∀𝑥𝑧 ∃!𝑦𝜑 → dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} = 𝑧)
11 vex 3234 . . . 4 𝑧 ∈ V
1210, 11syl6eqel 2738 . . 3 (∀𝑥𝑧 ∃!𝑦𝜑 → dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∈ V)
13 eumo 2527 . . . . . . 7 (∃!𝑦𝜑 → ∃*𝑦𝜑)
1413imim2i 16 . . . . . 6 ((𝑥𝑧 → ∃!𝑦𝜑) → (𝑥𝑧 → ∃*𝑦𝜑))
15 moanimv 2560 . . . . . 6 (∃*𝑦(𝑥𝑧𝜑) ↔ (𝑥𝑧 → ∃*𝑦𝜑))
1614, 15sylibr 224 . . . . 5 ((𝑥𝑧 → ∃!𝑦𝜑) → ∃*𝑦(𝑥𝑧𝜑))
1716alimi 1779 . . . 4 (∀𝑥(𝑥𝑧 → ∃!𝑦𝜑) → ∀𝑥∃*𝑦(𝑥𝑧𝜑))
18 df-ral 2946 . . . 4 (∀𝑥𝑧 ∃!𝑦𝜑 ↔ ∀𝑥(𝑥𝑧 → ∃!𝑦𝜑))
19 funopab 5961 . . . 4 (Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ↔ ∀𝑥∃*𝑦(𝑥𝑧𝜑))
2017, 18, 193imtr4i 281 . . 3 (∀𝑥𝑧 ∃!𝑦𝜑 → Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)})
21 funrnex 7175 . . 3 (dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∈ V → (Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} → ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∈ V))
2212, 20, 21sylc 65 . 2 (∀𝑥𝑧 ∃!𝑦𝜑 → ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∈ V)
23 nfra1 2970 . . 3 𝑥𝑥𝑧 ∃!𝑦𝜑
2410eleq2d 2716 . . . 4 (∀𝑥𝑧 ∃!𝑦𝜑 → (𝑥 ∈ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ↔ 𝑥𝑧))
25 opabid 5011 . . . . . . . . 9 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ↔ (𝑥𝑧𝜑))
26 vex 3234 . . . . . . . . . 10 𝑥 ∈ V
27 vex 3234 . . . . . . . . . 10 𝑦 ∈ V
2826, 27opelrn 5389 . . . . . . . . 9 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} → 𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)})
2925, 28sylbir 225 . . . . . . . 8 ((𝑥𝑧𝜑) → 𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)})
3029ex 449 . . . . . . 7 (𝑥𝑧 → (𝜑𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}))
3130impac 650 . . . . . 6 ((𝑥𝑧𝜑) → (𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∧ 𝜑))
3231eximi 1802 . . . . 5 (∃𝑦(𝑥𝑧𝜑) → ∃𝑦(𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∧ 𝜑))
337abeq2i 2764 . . . . 5 (𝑥 ∈ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ↔ ∃𝑦(𝑥𝑧𝜑))
34 df-rex 2947 . . . . 5 (∃𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑 ↔ ∃𝑦(𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∧ 𝜑))
3532, 33, 343imtr4i 281 . . . 4 (𝑥 ∈ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} → ∃𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑)
3624, 35syl6bir 244 . . 3 (∀𝑥𝑧 ∃!𝑦𝜑 → (𝑥𝑧 → ∃𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑))
3723, 36ralrimi 2986 . 2 (∀𝑥𝑧 ∃!𝑦𝜑 → ∀𝑥𝑧𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑)
38 nfopab1 4752 . . . . . 6 𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}
3938nfrn 5400 . . . . 5 𝑥ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}
4039nfeq2 2809 . . . 4 𝑥 𝑤 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}
41 nfcv 2793 . . . . 5 𝑦𝑤
42 nfopab2 4753 . . . . . 6 𝑦{⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}
4342nfrn 5400 . . . . 5 𝑦ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}
4441, 43rexeqf 3165 . . . 4 (𝑤 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} → (∃𝑦𝑤 𝜑 ↔ ∃𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑))
4540, 44ralbid 3012 . . 3 (𝑤 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} → (∀𝑥𝑧𝑦𝑤 𝜑 ↔ ∀𝑥𝑧𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑))
4645spcegv 3325 . 2 (ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∈ V → (∀𝑥𝑧𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑 → ∃𝑤𝑥𝑧𝑦𝑤 𝜑))
4722, 37, 46sylc 65 1 (∀𝑥𝑧 ∃!𝑦𝜑 → ∃𝑤𝑥𝑧𝑦𝑤 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wal 1521   = wceq 1523  wex 1744  wcel 2030  ∃!weu 2498  ∃*wmo 2499  {cab 2637  wral 2941  wrex 2942  {crab 2945  Vcvv 3231  cop 4216  {copab 4745  dom cdm 5143  ran crn 5144  Fun wfun 5920
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934
This theorem is referenced by:  bnj865  31119
  Copyright terms: Public domain W3C validator