ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  relelfvdm Unicode version

Theorem relelfvdm 5405
Description: If a function value has a member, the argument belongs to the domain. (Contributed by Jim Kingdon, 22-Jan-2019.)
Assertion
Ref Expression
relelfvdm  |-  ( ( Rel  F  /\  A  e.  ( F `  B
) )  ->  B  e.  dom  F )

Proof of Theorem relelfvdm
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elfv 5371 . . . . . 6  |-  ( A  e.  ( F `  B )  <->  E. x
( A  e.  x  /\  A. y ( B F y  <->  y  =  x ) ) )
2 exsimpr 1578 . . . . . 6  |-  ( E. x ( A  e.  x  /\  A. y
( B F y  <-> 
y  =  x ) )  ->  E. x A. y ( B F y  <->  y  =  x ) )
31, 2sylbi 120 . . . . 5  |-  ( A  e.  ( F `  B )  ->  E. x A. y ( B F y  <->  y  =  x ) )
4 equsb1 1739 . . . . . . . 8  |-  [ x  /  y ] y  =  x
5 spsbbi 1796 . . . . . . . 8  |-  ( A. y ( B F y  <->  y  =  x )  ->  ( [
x  /  y ] B F y  <->  [ x  /  y ] y  =  x ) )
64, 5mpbiri 167 . . . . . . 7  |-  ( A. y ( B F y  <->  y  =  x )  ->  [ x  /  y ] B F y )
7 nfv 1489 . . . . . . . 8  |-  F/ y  B F x
8 breq2 3897 . . . . . . . 8  |-  ( y  =  x  ->  ( B F y  <->  B F x ) )
97, 8sbie 1745 . . . . . . 7  |-  ( [ x  /  y ] B F y  <->  B F x )
106, 9sylib 121 . . . . . 6  |-  ( A. y ( B F y  <->  y  =  x )  ->  B F x )
1110eximi 1560 . . . . 5  |-  ( E. x A. y ( B F y  <->  y  =  x )  ->  E. x  B F x )
123, 11syl 14 . . . 4  |-  ( A  e.  ( F `  B )  ->  E. x  B F x )
1312anim2i 337 . . 3  |-  ( ( Rel  F  /\  A  e.  ( F `  B
) )  ->  ( Rel  F  /\  E. x  B F x ) )
14 19.42v 1858 . . 3  |-  ( E. x ( Rel  F  /\  B F x )  <-> 
( Rel  F  /\  E. x  B F x ) )
1513, 14sylibr 133 . 2  |-  ( ( Rel  F  /\  A  e.  ( F `  B
) )  ->  E. x
( Rel  F  /\  B F x ) )
16 releldm 4732 . . 3  |-  ( ( Rel  F  /\  B F x )  ->  B  e.  dom  F )
1716exlimiv 1558 . 2  |-  ( E. x ( Rel  F  /\  B F x )  ->  B  e.  dom  F )
1815, 17syl 14 1  |-  ( ( Rel  F  /\  A  e.  ( F `  B
) )  ->  B  e.  dom  F )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104   A.wal 1310   E.wex 1449    e. wcel 1461   [wsb 1716   class class class wbr 3893   dom cdm 4497   Rel wrel 4502   ` cfv 5079
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-sep 4004  ax-pow 4056  ax-pr 4089
This theorem depends on definitions:  df-bi 116  df-3an 945  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ral 2393  df-rex 2394  df-v 2657  df-un 3039  df-in 3041  df-ss 3048  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-br 3894  df-opab 3948  df-xp 4503  df-rel 4504  df-dm 4507  df-iota 5044  df-fv 5087
This theorem is referenced by:  mptrcl  5455  elfvmptrab1  5467  elmpocl  5920  oprssdmm  6020  mpoxopn0yelv  6087  eluzel2  9226  hashinfom  10410  istopon  12016  istps  12035  topontopn  12040  eltg4i  12060  eltg3  12062  tg1  12064  tg2  12065  tgclb  12070  cldrcl  12107  neiss2  12147  lmrcl  12196  cnprcl2k  12210  metflem  12331  xmetf  12332  ismet2  12336  xmeteq0  12341  xmettri2  12343  xmetpsmet  12351  xmetres2  12361  blfvalps  12367  blex  12369  blvalps  12370  blval  12371  blfps  12391  blf  12392  mopnval  12424  isxms2  12434  comet  12481
  Copyright terms: Public domain W3C validator