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

Theorem ralrn 5865
Description: Restricted universal quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario Carneiro, 20-Aug-2014.)
Hypothesis
Ref Expression
rexrn.1  |-  ( x  =  ( F `  y )  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
ralrn  |-  ( F  Fn  A  ->  ( A. x  e.  ran  F
ph 
<-> 
A. y  e.  A  ps ) )
Distinct variable groups:    x, y, A    x, F, y    ps, x    ph, y
Allowed substitution hints:    ph( x)    ps( y)

Proof of Theorem ralrn
StepHypRef Expression
1 fvex 5734 . . 3  |-  ( F `
 y )  e. 
_V
21a1i 11 . 2  |-  ( ( F  Fn  A  /\  y  e.  A )  ->  ( F `  y
)  e.  _V )
3 fvelrnb 5766 . . 3  |-  ( F  Fn  A  ->  (
x  e.  ran  F  <->  E. y  e.  A  ( F `  y )  =  x ) )
4 eqcom 2437 . . . 4  |-  ( ( F `  y )  =  x  <->  x  =  ( F `  y ) )
54rexbii 2722 . . 3  |-  ( E. y  e.  A  ( F `  y )  =  x  <->  E. y  e.  A  x  =  ( F `  y ) )
63, 5syl6bb 253 . 2  |-  ( F  Fn  A  ->  (
x  e.  ran  F  <->  E. y  e.  A  x  =  ( F `  y ) ) )
7 rexrn.1 . . 3  |-  ( x  =  ( F `  y )  ->  ( ph 
<->  ps ) )
87adantl 453 . 2  |-  ( ( F  Fn  A  /\  x  =  ( F `  y ) )  -> 
( ph  <->  ps ) )
92, 6, 8ralxfr2d 4731 1  |-  ( F  Fn  A  ->  ( A. x  e.  ran  F
ph 
<-> 
A. y  e.  A  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1652    e. wcel 1725   A.wral 2697   E.wrex 2698   _Vcvv 2948   ran crn 4871    Fn wfn 5441   ` cfv 5446
This theorem is referenced by:  ralrnmpt  5870  cbvfo  6014  isoselem  6053  indexfi  7406  ordtypelem9  7485  ordtypelem10  7486  wemapwe  7644  numacn  7920  acndom  7922  rpnnen1lem3  10592  fsequb2  11305  limsuple  12262  limsupval2  12264  climsup  12453  ruclem11  12829  ruclem12  12830  prmreclem6  13279  imasaddfnlem  13743  imasvscafn  13752  cycsubgcl  14956  ghmrn  15009  ghmnsgima  15019  pgpssslw  15238  gexex  15458  dprdfcntz  15563  znf1o  16822  ptcnplem  17643  kqt0lem  17758  isr0  17759  regr1lem2  17762  uzrest  17919  tmdgsum2  18116  imasf1oxmet  18395  imasf1omet  18396  bndth  18973  evth  18974  ovolficcss  19356  ovollb2lem  19374  ovolunlem1  19383  ovoliunlem1  19388  ovoliunlem2  19389  ovoliun2  19392  ovolscalem1  19399  ovolicc1  19402  voliunlem2  19435  voliunlem3  19436  ioombl1lem4  19445  uniioovol  19461  uniioombllem2  19465  uniioombllem3  19467  uniioombllem6  19470  volsup2  19487  vitalilem3  19492  mbfsup  19546  mbfinf  19547  mbflimsup  19548  itg1ge0  19568  itg1mulc  19586  itg1climres  19596  mbfi1fseqlem4  19600  itg2seq  19624  itg2monolem1  19632  itg2mono  19635  itg2i1fseq2  19638  itg2gt0  19642  itg2cnlem1  19643  itg2cn  19645  limciun  19771  plycpn  20196  hmopidmchi  23644  hmopidmpji  23645  rge0scvg  24325  mblfinlem  26207  ismtyhmeolem  26467  nacsfix  26720  fnwe2lem2  27080  frlmlbs  27181  lindfrn  27223  climinf  27663
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-iota 5410  df-fun 5448  df-fn 5449  df-fv 5454
  Copyright terms: Public domain W3C validator