| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > funimaexg | Structured version Visualization version GIF version | ||
| 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.) |
| Ref | Expression |
|---|---|
| funimaexg | ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 “ 𝐵) ∈ V) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dffun6 6536 | . . . 4 ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∃*𝑦 𝑥𝐴𝑦)) | |
| 2 | 1 | simprbi 502 | . . 3 ⊢ (Fun 𝐴 → ∀𝑥∃*𝑦 𝑥𝐴𝑦) |
| 3 | dfima2 6054 | . . . 4 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑥𝐴𝑦} | |
| 4 | axrep6g 5244 | . . . 4 ⊢ ((𝐵 ∈ 𝐶 ∧ ∀𝑥∃*𝑦 𝑥𝐴𝑦) → {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑥𝐴𝑦} ∈ V) | |
| 5 | 3, 4 | eqeltrid 2869 | . . 3 ⊢ ((𝐵 ∈ 𝐶 ∧ ∀𝑥∃*𝑦 𝑥𝐴𝑦) → (𝐴 “ 𝐵) ∈ V) |
| 6 | 2, 5 | sylan2 604 | . 2 ⊢ ((𝐵 ∈ 𝐶 ∧ Fun 𝐴) → (𝐴 “ 𝐵) ∈ V) |
| 7 | 6 | ancoms 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 5104 “ cima 5654 Rel wrel 5656 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 5231 ax-sep 5250 ax-pr 5394 |
| 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 5105 df-opab 5167 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 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 12223 seqex 14027 fbasrn 23998 elfm3 24064 bdayimaon 27811 nosupno 27821 noinfno 27836 noeta2 27908 etaslts2 27941 cutbdaybnd2lim 27944 madeval 27979 oldval 27981 negsunif 28202 bdayons 28423 n0sexg 28463 fnimafnex 44023 fundcmpsurinjlem3 48005 fundcmpsurbijinjpreimafv 48012 fundcmpsurbijinj 48015 fundcmpsurinjALT 48017 grimuhgr 48508 |
| Copyright terms: Public domain | W3C validator |