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

Theorem resiexg 7247
Description: The existence of a restricted identity function, proved without using the Axiom of Replacement (unlike resfunexg 6621). (Contributed by NM, 13-Jan-2007.)
Assertion
Ref Expression
resiexg (𝐴𝑉 → ( I ↾ 𝐴) ∈ V)

Proof of Theorem resiexg
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relres 5565 . . 3 Rel ( I ↾ 𝐴)
2 simpr 471 . . . . 5 ((𝑥 = 𝑦𝑥𝐴) → 𝑥𝐴)
3 eleq1w 2833 . . . . . 6 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
43biimpa 462 . . . . 5 ((𝑥 = 𝑦𝑥𝐴) → 𝑦𝐴)
52, 4jca 501 . . . 4 ((𝑥 = 𝑦𝑥𝐴) → (𝑥𝐴𝑦𝐴))
6 vex 3354 . . . . . 6 𝑦 ∈ V
76opelres 5540 . . . . 5 (⟨𝑥, 𝑦⟩ ∈ ( I ↾ 𝐴) ↔ (⟨𝑥, 𝑦⟩ ∈ I ∧ 𝑥𝐴))
8 df-br 4787 . . . . . . 7 (𝑥 I 𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ I )
96ideq 5411 . . . . . . 7 (𝑥 I 𝑦𝑥 = 𝑦)
108, 9bitr3i 266 . . . . . 6 (⟨𝑥, 𝑦⟩ ∈ I ↔ 𝑥 = 𝑦)
1110anbi1i 610 . . . . 5 ((⟨𝑥, 𝑦⟩ ∈ I ∧ 𝑥𝐴) ↔ (𝑥 = 𝑦𝑥𝐴))
127, 11bitri 264 . . . 4 (⟨𝑥, 𝑦⟩ ∈ ( I ↾ 𝐴) ↔ (𝑥 = 𝑦𝑥𝐴))
13 opelxp 5284 . . . 4 (⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐴) ↔ (𝑥𝐴𝑦𝐴))
145, 12, 133imtr4i 281 . . 3 (⟨𝑥, 𝑦⟩ ∈ ( I ↾ 𝐴) → ⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐴))
151, 14relssi 5349 . 2 ( I ↾ 𝐴) ⊆ (𝐴 × 𝐴)
16 sqxpexg 7108 . 2 (𝐴𝑉 → (𝐴 × 𝐴) ∈ V)
17 ssexg 4938 . 2 ((( I ↾ 𝐴) ⊆ (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ∈ V) → ( I ↾ 𝐴) ∈ V)
1815, 16, 17sylancr 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