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.

Step	Hyp	Ref	Expression
1		dffun6 6536	. . . 4 ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∃*𝑦 𝑥𝐴𝑦))
2	1	simprbi 502	. . 3 ⊢ (Fun 𝐴 → ∀𝑥∃*𝑦 𝑥𝐴𝑦)
3		dfima2 6055	. . . 4 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑥𝐴𝑦}
4		axrep6g 5245	. . . 4 ⊢ ((𝐵 ∈ 𝐶 ∧ ∀𝑥∃*𝑦 𝑥𝐴𝑦) → {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑥𝐴𝑦} ∈ V)
5	3, 4	eqeltrid 2869	. . 3 ⊢ ((𝐵 ∈ 𝐶 ∧ ∀𝑥∃*𝑦 𝑥𝐴𝑦) → (𝐴 “ 𝐵) ∈ V)
6	2, 5	sylan2 604	. 2 ⊢ ((𝐵 ∈ 𝐶 ∧ Fun 𝐴) → (𝐴 “ 𝐵) ∈ V)
7	6	ancoms 463	1 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 “ 𝐵) ∈ V)

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