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

Theorem ralrn 5812
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 5682 . . 3  |-  ( F `
 y )  e. 
_V
21a1i 11 . 2  |-  ( ( F  Fn  A  /\  y  e.  A )  ->  ( F `  y
)  e.  _V )
3 fvelrnb 5713 . . 3  |-  ( F  Fn  A  ->  (
x  e.  ran  F  <->  E. y  e.  A  ( F `  y )  =  x ) )
4 eqcom 2389 . . . 4  |-  ( ( F `  y )  =  x  <->  x  =  ( F `  y ) )
54rexbii 2674 . . 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 4679 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 1649    e. wcel 1717   A.wral 2649   E.wrex 2650   _Vcvv 2899   ran crn 4819    Fn wfn 5389   ` cfv 5394
This theorem is referenced by:  ralrnmpt  5817  cbvfo  5961  isoselem  6000  indexfi  7349  ordtypelem9  7428  ordtypelem10  7429  wemapwe  7587  numacn  7863  acndom  7865  rpnnen1lem3  10534  fsequb2  11242  limsuple  12199  limsupval2  12201  climsup  12390  ruclem11  12766  ruclem12  12767  prmreclem6  13216  imasaddfnlem  13680  imasvscafn  13689  cycsubgcl  14893  ghmrn  14946  ghmnsgima  14956  pgpssslw  15175  gexex  15395  dprdfcntz  15500  znf1o  16755  ptcnplem  17574  kqt0lem  17689  isr0  17690  regr1lem2  17693  uzrest  17850  tmdgsum2  18047  imasf1oxmet  18313  imasf1omet  18314  bndth  18854  evth  18855  ovolficcss  19233  ovollb2lem  19251  ovolunlem1  19260  ovoliunlem1  19265  ovoliunlem2  19266  ovoliun2  19269  ovolscalem1  19276  ovolicc1  19279  voliunlem2  19312  voliunlem3  19313  ioombl1lem4  19322  uniioovol  19338  uniioombllem2  19342  uniioombllem3  19344  uniioombllem6  19347  volsup2  19364  vitalilem3  19369  mbfsup  19423  mbfinf  19424  mbflimsup  19425  itg1ge0  19445  itg1mulc  19463  itg1climres  19473  mbfi1fseqlem4  19477  itg2seq  19501  itg2monolem1  19509  itg2mono  19512  itg2i1fseq2  19515  itg2gt0  19519  itg2cnlem1  19520  itg2cn  19522  limciun  19648  plycpn  20073  hmopidmchi  23502  hmopidmpji  23503  rge0scvg  24139  ismtyhmeolem  26204  nacsfix  26457  fnwe2lem2  26817  frlmlbs  26918  lindfrn  26960  climinf  27400
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pr 4344
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-rab 2658  df-v 2901  df-sbc 3105  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-br 4154  df-opab 4208  df-mpt 4209  df-id 4439  df-xp 4824  df-rel 4825  df-cnv 4826  df-co 4827  df-dm 4828  df-rn 4829  df-iota 5358  df-fun 5396  df-fn 5397  df-fv 5402
  Copyright terms: Public domain W3C validator