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

Theorem resiexg 6729
Description: The existence of a restricted identity function, proved without using the Axiom of Replacement (unlike resfunexg 6130). (Contributed by NM, 13-Jan-2007.)
Assertion
Ref Expression
resiexg  |-  ( A  e.  V  ->  (  _I  |`  A )  e. 
_V )

Proof of Theorem resiexg
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relres 5132 . . 3  |-  Rel  (  _I  |`  A )
2 simpr 463 . . . . 5  |-  ( ( x  =  y  /\  x  e.  A )  ->  x  e.  A )
3 eleq1 2517 . . . . . 6  |-  ( x  =  y  ->  (
x  e.  A  <->  y  e.  A ) )
43biimpa 487 . . . . 5  |-  ( ( x  =  y  /\  x  e.  A )  ->  y  e.  A )
52, 4jca 535 . . . 4  |-  ( ( x  =  y  /\  x  e.  A )  ->  ( x  e.  A  /\  y  e.  A
) )
6 vex 3048 . . . . . 6  |-  y  e. 
_V
76opelres 5110 . . . . 5  |-  ( <.
x ,  y >.  e.  (  _I  |`  A )  <-> 
( <. x ,  y
>.  e.  _I  /\  x  e.  A ) )
8 df-br 4403 . . . . . . 7  |-  ( x  _I  y  <->  <. x ,  y >.  e.  _I  )
96ideq 4987 . . . . . . 7  |-  ( x  _I  y  <->  x  =  y )
108, 9bitr3i 255 . . . . . 6  |-  ( <.
x ,  y >.  e.  _I  <->  x  =  y
)
1110anbi1i 701 . . . . 5  |-  ( (
<. x ,  y >.  e.  _I  /\  x  e.  A )  <->  ( x  =  y  /\  x  e.  A ) )
127, 11bitri 253 . . . 4  |-  ( <.
x ,  y >.  e.  (  _I  |`  A )  <-> 
( x  =  y  /\  x  e.  A
) )
13 opelxp 4864 . . . 4  |-  ( <.
x ,  y >.  e.  ( A  X.  A
)  <->  ( x  e.  A  /\  y  e.  A ) )
145, 12, 133imtr4i 270 . . 3  |-  ( <.
x ,  y >.  e.  (  _I  |`  A )  ->  <. x ,  y
>.  e.  ( A  X.  A ) )
151, 14relssi 4926 . 2  |-  (  _I  |`  A )  C_  ( A  X.  A )
16 sqxpexg 6596 . 2  |-  ( A  e.  V  ->  ( A  X.  A )  e. 
_V )
17 ssexg 4549 . 2  |-  ( ( (  _I  |`  A ) 
C_  ( A  X.  A )  /\  ( A  X.  A )  e. 
_V )  ->  (  _I  |`  A )  e. 
_V )
1815, 16, 17sylancr 669 1  |-  ( A  e.  V  ->  (  _I  |`  A )  e. 
_V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    e. wcel 1887   _Vcvv 3045    C_ wss 3404   <.cop 3974   class class class wbr 4402    _I cid 4744    X. cxp 4832    |` cres 4836
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-id 4749  df-xp 4840  df-rel 4841  df-res 4846
This theorem is referenced by:  ordiso  8031  wdomref  8087  dfac9  8566  relexp0g  13085  relexpsucnnr  13088  ndxarg  15141  idfu2nd  15782  idfu1st  15784  idfucl  15786  setcid  15981  equivestrcsetc  16037  pf1ind  18943  islinds2  19371  ausisusgra  25082  cusgraexilem1  25194  sizeusglecusg  25214  poimirlem15  31955  dib0  34732  dicn0  34760  cdlemn11a  34775  dihord6apre  34824  dihatlat  34902  dihpN  34904  eldioph2lem1  35602  eldioph2lem2  35603  dfrtrcl5  36236  dfrcl2  36266  relexpiidm  36296  ausgrusgrb  39252  upgrres1lem1  39376  usgrexi  39506  sizusglecusg  39524  rngcidALTV  40046  ringcidALTV  40109
  Copyright terms: Public domain W3C validator