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

Theorem funimaexg 6612
Description: Axiom of Replacement using abbreviations. Axiom 39(vi) of [Quine] p. 284. Compare Exercise 9 of [TakeutiZaring] p. 29. (Contributed by NM, 10-Sep-2006.) Shorten proof and avoid ax-10 2178, ax-12 2215. (Revised by SN, 19-Dec-2024.)
Assertion
Ref Expression
funimaexg ((Fun 𝐴𝐵𝐶) → (𝐴𝐵) ∈ V)

Proof of Theorem funimaexg
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dffun6 6536 . . . 4 (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∃*𝑦 𝑥𝐴𝑦))
21simprbi 502 . . 3 (Fun 𝐴 → ∀𝑥∃*𝑦 𝑥𝐴𝑦)
3 dfima2 6055 . . . 4 (𝐴𝐵) = {𝑦 ∣ ∃𝑥𝐵 𝑥𝐴𝑦}
4 axrep6g 5245 . . . 4 ((𝐵𝐶 ∧ ∀𝑥∃*𝑦 𝑥𝐴𝑦) → {𝑦 ∣ ∃𝑥𝐵 𝑥𝐴𝑦} ∈ V)
53, 4eqeltrid 2869 . . 3 ((𝐵𝐶 ∧ ∀𝑥∃*𝑦 𝑥𝐴𝑦) → (𝐴𝐵) ∈ V)
62, 5sylan2 604 . 2 ((𝐵𝐶 ∧ Fun 𝐴) → (𝐴𝐵) ∈ V)
76ancoms 463 1 ((Fun 𝐴𝐵𝐶) → (𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 400  wal 1561  wcel 2145  ∃*wmo 2567  {cab 2743  wrex 3089  Vcvv 3457   class class class wbr 5105  cima 5655  Rel wrel 5657  Fun wfun 6519
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-rep 5232  ax-sep 5251  ax-pr 5395
This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-mo 2569  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-opab 5168  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-fun 6527
This theorem is referenced by:  funimaex  6613  resfunexg  7203  resfunexgALT  7933  fnexALT  7936  naddcllem  8650  naddunif  8668  wdomimag  9537  carduniima  10068  dfac12lem2  10116  ttukeylem3  10483  nnexALT  12226  seqex  14030  fbasrn  24002  elfm3  24068  bdayimaon  27815  nosupno  27825  noinfno  27840  noeta2  27912  etaslts2  27945  cutbdaybnd2lim  27948  madeval  27983  oldval  27985  negsunif  28206  bdayons  28427  n0sexg  28467  fnimafnex  44028  fundcmpsurinjlem3  48004  fundcmpsurbijinjpreimafv  48011  fundcmpsurbijinj  48014  fundcmpsurinjALT  48016  grimuhgr  48507
  Copyright terms: Public domain W3C validator