![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > resiexg | Structured version Visualization version GIF version |
Description: The existence of a restricted identity function, proved without using the Axiom of Replacement (unlike resfunexg 6621). (Contributed by NM, 13-Jan-2007.) |
Ref | Expression |
---|---|
resiexg | ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relres 5565 | . . 3 ⊢ Rel ( I ↾ 𝐴) | |
2 | simpr 471 | . . . . 5 ⊢ ((𝑥 = 𝑦 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) | |
3 | eleq1w 2833 | . . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | |
4 | 3 | biimpa 462 | . . . . 5 ⊢ ((𝑥 = 𝑦 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴) |
5 | 2, 4 | jca 501 | . . . 4 ⊢ ((𝑥 = 𝑦 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) |
6 | vex 3354 | . . . . . 6 ⊢ 𝑦 ∈ V | |
7 | 6 | opelres 5540 | . . . . 5 ⊢ (〈𝑥, 𝑦〉 ∈ ( I ↾ 𝐴) ↔ (〈𝑥, 𝑦〉 ∈ I ∧ 𝑥 ∈ 𝐴)) |
8 | df-br 4787 | . . . . . . 7 ⊢ (𝑥 I 𝑦 ↔ 〈𝑥, 𝑦〉 ∈ I ) | |
9 | 6 | ideq 5411 | . . . . . . 7 ⊢ (𝑥 I 𝑦 ↔ 𝑥 = 𝑦) |
10 | 8, 9 | bitr3i 266 | . . . . . 6 ⊢ (〈𝑥, 𝑦〉 ∈ I ↔ 𝑥 = 𝑦) |
11 | 10 | anbi1i 610 | . . . . 5 ⊢ ((〈𝑥, 𝑦〉 ∈ I ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝑦 ∧ 𝑥 ∈ 𝐴)) |
12 | 7, 11 | bitri 264 | . . . 4 ⊢ (〈𝑥, 𝑦〉 ∈ ( I ↾ 𝐴) ↔ (𝑥 = 𝑦 ∧ 𝑥 ∈ 𝐴)) |
13 | opelxp 5284 | . . . 4 ⊢ (〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) | |
14 | 5, 12, 13 | 3imtr4i 281 | . . 3 ⊢ (〈𝑥, 𝑦〉 ∈ ( I ↾ 𝐴) → 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐴)) |
15 | 1, 14 | relssi 5349 | . 2 ⊢ ( I ↾ 𝐴) ⊆ (𝐴 × 𝐴) |
16 | sqxpexg 7108 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 × 𝐴) ∈ V) | |
17 | ssexg 4938 | . 2 ⊢ ((( I ↾ 𝐴) ⊆ (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ∈ V) → ( I ↾ 𝐴) ∈ V) | |
18 | 15, 16, 17 | sylancr 575 | 1 ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 ∈ wcel 2145 Vcvv 3351 ⊆ wss 3723 〈cop 4322 class class class wbr 4786 I cid 5156 × cxp 5247 ↾ cres 5251 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-sep 4915 ax-nul 4923 ax-pow 4974 ax-pr 5034 ax-un 7094 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3353 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-nul 4064 df-if 4226 df-pw 4299 df-sn 4317 df-pr 4319 df-op 4323 df-uni 4575 df-br 4787 df-opab 4847 df-id 5157 df-xp 5255 df-rel 5256 df-res 5261 |
This theorem is referenced by: ordiso 8575 wdomref 8631 dfac9 9158 relexp0g 13963 relexpsucnnr 13966 ndxarg 16082 idfu2nd 16737 idfu1st 16739 idfucl 16741 setcid 16936 equivestrcsetc 16993 pf1ind 19927 islinds2 20362 ausgrusgrb 26275 upgrres1lem1 26417 cusgrexilem1 26563 sizusglecusg 26587 pliguhgr 27673 bj-evalid 33353 poimirlem15 33750 xrnidresex 34500 dib0 36967 dicn0 36995 cdlemn11a 37010 dihord6apre 37059 dihatlat 37137 dihpN 37139 eldioph2lem1 37842 eldioph2lem2 37843 dfrtrcl5 38455 dfrcl2 38485 relexpiidm 38515 uspgrsprfo 42277 rngcidALTV 42512 ringcidALTV 42575 |
Copyright terms: Public domain | W3C validator |