Theorem ralrn 6048

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

Step	Hyp	Ref	Expression
1		fvex 5898	. . 3 |- ( F ` y ) e. _V
2	1	a1i 11	. 2 |- ( ( F Fn A /\ y e. A ) -> ( F ` y ) e. _V )
3		fvelrnb 5935	. . 3 |- ( F Fn A -> ( x e. ran F <-> E. y e. A ( F ` y ) = x ) )
4		eqcom 2469	. . . 4 |- ( ( F ` y ) = x <-> x = ( F ` y ) )
5	4	rexbii 2901	. . 3 |- ( E. y e. A ( F ` y ) = x <-> E. y e. A x = ( F ` y ) )
6	3, 5	syl6bb 269	. 2 |- ( F Fn A -> ( x e. ran F <-> E. y e. A x = ( F ` y ) ) )
7		rexrn.1	. . 3 |- ( x = ( F ` y ) -> ( ph <-> ps ) )
8	7	adantl 472	. 2 |- ( ( F Fn A /\ x = ( F ` y ) ) -> ( ph <-> ps ) )
9	2, 6, 8	ralxfr2d 4630	1 |- ( F Fn A -> ( A. x e. ran F ph <-> A. y e. A ps ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   = wceq 1455   e. wcel 1898   A.wral 2749   E.wrex 2750   _Vcvv 3057   ran crn 4854   Fn wfn 5596   ` cfv 5601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pr 4653

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-iota 5565  df-fun 5603  df-fn 5604  df-fv 5609

This theorem is referenced by:  ralrnmpt  6054  cbvfo  6212  isoselem  6257  indexfi  7908  ordtypelem9  8067  ordtypelem10  8068  wemapwe  8228  numacn  8506  acndom  8508  rpnnen1lem3  11321  fsequb2  12221  limsuple  13585  limsupleOLD  13586  limsupval2  13589  limsupval2OLD  13590  climsup  13782  ruclem11  14341  ruclem12  14342  prmreclem6  14914  imasaddfnlem  15483  imasvscafn  15492  cycsubgcl  16892  ghmrn  16945  ghmnsgima  16955  pgpssslw  17315  gexex  17540  dprdfcntz  17697  znf1o  19171  frlmlbs  19404  lindfrn  19428  ptcnplem  20685  kqt0lem  20800  isr0  20801  regr1lem2  20804  uzrest  20961  tmdgsum2  21160  imasf1oxmet  21439  imasf1omet  21440  bndth  22035  evth  22036  ovolficcss  22471  ovollb2lem  22490  ovolunlem1  22499  ovoliunlem1  22504  ovoliunlem2  22505  ovoliun2  22508  ovolscalem1  22515  ovolicc1  22518  voliunlem2  22553  voliunlem3  22554  ioombl1lem4  22563  uniioovol  22585  uniioombllem2  22589  uniioombllem2OLD  22590  uniioombllem3  22592  uniioombllem6  22595  volsup2  22612  vitalilem3  22617  mbfsup  22669  mbfinf  22670  mbfinfOLD  22671  mbflimsup  22672  mbflimsupOLD  22673  itg1ge0  22693  itg1mulc  22711  itg1climres  22721  mbfi1fseqlem4  22725  itg2seq  22749  itg2monolem1  22757  itg2mono  22760  itg2i1fseq2  22763  itg2gt0  22767  itg2cnlem1  22768  itg2cn  22770  limciun  22898  plycpn  23291  hmopidmchi  27853  hmopidmpji  27854  rge0scvg  28804  mclsax  30256  mblfinlem2  32023  ismtyhmeolem  32181  nacsfix  35599  fnwe2lem2  35954  climinf  37722  climinfOLD  37723