Theorem ralrn 6019

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 5866	. . 3 |- ( F ` y ) e. _V
2	1	a1i 11	. 2 |- ( ( F Fn A /\ y e. A ) -> ( F ` y ) e. _V )
3		fvelrnb 5905	. . 3 |- ( F Fn A -> ( x e. ran F <-> E. y e. A ( F ` y ) = x ) )
4		eqcom 2452	. . . 4 |- ( ( F ` y ) = x <-> x = ( F ` y ) )
5	4	rexbii 2945	. . 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 466	. 2 |- ( ( F Fn A /\ x = ( F ` y ) ) -> ( ph <-> ps ) )
9	2, 6, 8	ralxfr2d 4653	1 |- ( F Fn A -> ( A. x e. ran F ph <-> A. y e. A ps ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1383   e. wcel 1804   A.wral 2793   E.wrex 2794   _Vcvv 3095   ran crn 4990   Fn wfn 5573   ` cfv 5578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-iota 5541  df-fun 5580  df-fn 5581  df-fv 5586

This theorem is referenced by:  ralrnmpt  6025  cbvfo  6177  isoselem  6222  indexfi  7830  ordtypelem9  7954  ordtypelem10  7955  wemapwe  8142  wemapweOLD  8143  numacn  8433  acndom  8435  rpnnen1lem3  11219  fsequb2  12065  limsuple  13280  limsupval2  13282  climsup  13471  ruclem11  13850  ruclem12  13851  prmreclem6  14316  imasaddfnlem  14802  imasvscafn  14811  cycsubgcl  16101  ghmrn  16154  ghmnsgima  16164  pgpssslw  16508  gexex  16733  dprdfcntz  16923  dprdfcntzOLD  16929  znf1o  18463  frlmlbs  18704  lindfrn  18729  ptcnplem  19995  kqt0lem  20110  isr0  20111  regr1lem2  20114  uzrest  20271  tmdgsum2  20468  imasf1oxmet  20751  imasf1omet  20752  bndth  21331  evth  21332  ovolficcss  21754  ovollb2lem  21772  ovolunlem1  21781  ovoliunlem1  21786  ovoliunlem2  21787  ovoliun2  21790  ovolscalem1  21797  ovolicc1  21800  voliunlem2  21834  voliunlem3  21835  ioombl1lem4  21844  uniioovol  21861  uniioombllem2  21865  uniioombllem3  21867  uniioombllem6  21870  volsup2  21887  vitalilem3  21892  mbfsup  21944  mbfinf  21945  mbflimsup  21946  itg1ge0  21966  itg1mulc  21984  itg1climres  21994  mbfi1fseqlem4  21998  itg2seq  22022  itg2monolem1  22030  itg2mono  22033  itg2i1fseq2  22036  itg2gt0  22040  itg2cnlem1  22041  itg2cn  22043  limciun  22171  plycpn  22557  hmopidmchi  26942  hmopidmpji  26943  rge0scvg  27804  mclsax  28802  mblfinlem2  30027  ismtyhmeolem  30275  nacsfix  30619  fnwe2lem2  30972  climinf  31520