![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imadmrn | Structured version Visualization version GIF version |
Description: The image of the domain of a class is the range of the class. (Contributed by NM, 14-Aug-1994.) |
Ref | Expression |
---|---|
imadmrn | ⊢ (𝐴 “ dom 𝐴) = ran 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3440 | . . . . . . 7 ⊢ 𝑥 ∈ V | |
2 | vex 3440 | . . . . . . 7 ⊢ 𝑦 ∈ V | |
3 | 1, 2 | opeldm 5662 | . . . . . 6 ⊢ (〈𝑥, 𝑦〉 ∈ 𝐴 → 𝑥 ∈ dom 𝐴) |
4 | 3 | pm4.71i 560 | . . . . 5 ⊢ (〈𝑥, 𝑦〉 ∈ 𝐴 ↔ (〈𝑥, 𝑦〉 ∈ 𝐴 ∧ 𝑥 ∈ dom 𝐴)) |
5 | ancom 461 | . . . . 5 ⊢ ((〈𝑥, 𝑦〉 ∈ 𝐴 ∧ 𝑥 ∈ dom 𝐴) ↔ (𝑥 ∈ dom 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ 𝐴)) | |
6 | 4, 5 | bitr2i 277 | . . . 4 ⊢ ((𝑥 ∈ dom 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ 𝐴) ↔ 〈𝑥, 𝑦〉 ∈ 𝐴) |
7 | 6 | exbii 1829 | . . 3 ⊢ (∃𝑥(𝑥 ∈ dom 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ 𝐴) ↔ ∃𝑥〈𝑥, 𝑦〉 ∈ 𝐴) |
8 | 7 | abbii 2861 | . 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ dom 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ 𝐴)} = {𝑦 ∣ ∃𝑥〈𝑥, 𝑦〉 ∈ 𝐴} |
9 | dfima3 5809 | . 2 ⊢ (𝐴 “ dom 𝐴) = {𝑦 ∣ ∃𝑥(𝑥 ∈ dom 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ 𝐴)} | |
10 | dfrn3 5646 | . 2 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥〈𝑥, 𝑦〉 ∈ 𝐴} | |
11 | 8, 9, 10 | 3eqtr4i 2829 | 1 ⊢ (𝐴 “ dom 𝐴) = ran 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 396 = wceq 1522 ∃wex 1761 ∈ wcel 2081 {cab 2775 〈cop 4478 dom cdm 5443 ran crn 5444 “ cima 5446 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5094 ax-nul 5101 ax-pr 5221 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-sn 4473 df-pr 4475 df-op 4479 df-br 4963 df-opab 5025 df-xp 5449 df-cnv 5451 df-dm 5453 df-rn 5454 df-res 5455 df-ima 5456 |
This theorem is referenced by: cnvimarndm 5826 foima 6463 fimadmfo 6467 f1imacnv 6499 fsn2 6761 resfunexg 6844 elunirnALT 6876 fnexALT 7508 uniqs2 8209 mapsnd 8299 phplem4 8546 php3 8550 jech9.3 9089 fin4en1 9577 retopbas 23052 plyeq0 24484 rnelshi 29527 s2rn 30300 s3rn 30302 poimirlem3 34426 poimirlem30 34453 |
Copyright terms: Public domain | W3C validator |