Theorem ralrn 5936

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 5784	. . 3 |- ( F ` y ) e. _V
2	1	a1i 11	. 2 |- ( ( F Fn A /\ y e. A ) -> ( F ` y ) e. _V )
3		fvelrnb 5821	. . 3 |- ( F Fn A -> ( x e. ran F <-> E. y e. A ( F ` y ) = x ) )
4		eqcom 2391	. . . 4 |- ( ( F ` y ) = x <-> x = ( F ` y ) )
5	4	rexbii 2884	. . 3 |- ( E. y e. A ( F ` y ) = x <-> E. y e. A x = ( F ` y ) )
6	3, 5	syl6bb 261	. 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 464	. 2 |- ( ( F Fn A /\ x = ( F ` y ) ) -> ( ph <-> ps ) )
9	2, 6, 8	ralxfr2d 4578	1 |- ( F Fn A -> ( A. x e. ran F ph <-> A. y e. A ps ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 367   = wceq 1399   e. wcel 1826   A.wral 2732   E.wrex 2733   _Vcvv 3034   ran crn 4914   Fn wfn 5491   ` cfv 5496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pr 4601

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-sbc 3253  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-opab 4426  df-mpt 4427  df-id 4709  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-iota 5460  df-fun 5498  df-fn 5499  df-fv 5504

This theorem is referenced by:  ralrnmpt  5942  cbvfo  6093  isoselem  6138  indexfi  7743  ordtypelem9  7866  ordtypelem10  7867  wemapwe  8052  wemapweOLD  8053  numacn  8343  acndom  8345  rpnnen1lem3  11129  fsequb2  11989  limsuple  13303  limsupval2  13305  climsup  13494  ruclem11  13975  ruclem12  13976  prmreclem6  14441  imasaddfnlem  14935  imasvscafn  14944  cycsubgcl  16344  ghmrn  16397  ghmnsgima  16407  pgpssslw  16751  gexex  16976  dprdfcntz  17162  dprdfcntzOLD  17168  znf1o  18681  frlmlbs  18917  lindfrn  18941  ptcnplem  20207  kqt0lem  20322  isr0  20323  regr1lem2  20326  uzrest  20483  tmdgsum2  20680  imasf1oxmet  20963  imasf1omet  20964  bndth  21543  evth  21544  ovolficcss  21966  ovollb2lem  21984  ovolunlem1  21993  ovoliunlem1  21998  ovoliunlem2  21999  ovoliun2  22002  ovolscalem1  22009  ovolicc1  22012  voliunlem2  22046  voliunlem3  22047  ioombl1lem4  22056  uniioovol  22073  uniioombllem2  22077  uniioombllem3  22079  uniioombllem6  22082  volsup2  22099  vitalilem3  22104  mbfsup  22156  mbfinf  22157  mbflimsup  22158  itg1ge0  22178  itg1mulc  22196  itg1climres  22206  mbfi1fseqlem4  22210  itg2seq  22234  itg2monolem1  22242  itg2mono  22245  itg2i1fseq2  22248  itg2gt0  22252  itg2cnlem1  22253  itg2cn  22255  limciun  22383  plycpn  22770  hmopidmchi  27186  hmopidmpji  27187  rge0scvg  28085  mclsax  29118  mblfinlem2  30217  ismtyhmeolem  30466  nacsfix  30810  fnwe2lem2  31163  climinf  31778