Theorem ralrn 5851

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 5706	. . 3 |- ( F ` y ) e. _V
2	1	a1i 11	. 2 |- ( ( F Fn A /\ y e. A ) -> ( F ` y ) e. _V )
3		fvelrnb 5744	. . 3 |- ( F Fn A -> ( x e. ran F <-> E. y e. A ( F ` y ) = x ) )
4		eqcom 2445	. . . 4 |- ( ( F ` y ) = x <-> x = ( F ` y ) )
5	4	rexbii 2745	. . 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 4513	1 |- ( F Fn A -> ( A. x e. ran F ph <-> A. y e. A ps ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1369   e. wcel 1756   A.wral 2720   E.wrex 2721   _Vcvv 2977   ran crn 4846   Fn wfn 5418   ` cfv 5423

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418  ax-nul 4426  ax-pr 4536

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-ral 2725  df-rex 2726  df-rab 2729  df-v 2979  df-sbc 3192  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-sn 3883  df-pr 3885  df-op 3889  df-uni 4097  df-br 4298  df-opab 4356  df-mpt 4357  df-id 4641  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-iota 5386  df-fun 5425  df-fn 5426  df-fv 5431

This theorem is referenced by:  ralrnmpt  5857  cbvfo  5998  isoselem  6037  indexfi  7624  ordtypelem9  7745  ordtypelem10  7746  wemapwe  7933  wemapweOLD  7934  numacn  8224  acndom  8226  rpnnen1lem3  10986  fsequb2  11803  limsuple  12961  limsupval2  12963  climsup  13152  ruclem11  13527  ruclem12  13528  prmreclem6  13987  imasaddfnlem  14471  imasvscafn  14480  cycsubgcl  15712  ghmrn  15765  ghmnsgima  15775  pgpssslw  16118  gexex  16340  dprdfcntz  16504  dprdfcntzOLD  16510  znf1o  17989  frlmlbs  18230  lindfrn  18255  ptcnplem  19199  kqt0lem  19314  isr0  19315  regr1lem2  19318  uzrest  19475  tmdgsum2  19672  imasf1oxmet  19955  imasf1omet  19956  bndth  20535  evth  20536  ovolficcss  20958  ovollb2lem  20976  ovolunlem1  20985  ovoliunlem1  20990  ovoliunlem2  20991  ovoliun2  20994  ovolscalem1  21001  ovolicc1  21004  voliunlem2  21037  voliunlem3  21038  ioombl1lem4  21047  uniioovol  21064  uniioombllem2  21068  uniioombllem3  21070  uniioombllem6  21073  volsup2  21090  vitalilem3  21095  mbfsup  21147  mbfinf  21148  mbflimsup  21149  itg1ge0  21169  itg1mulc  21187  itg1climres  21197  mbfi1fseqlem4  21201  itg2seq  21225  itg2monolem1  21233  itg2mono  21236  itg2i1fseq2  21239  itg2gt0  21243  itg2cnlem1  21244  itg2cn  21246  limciun  21374  plycpn  21760  hmopidmchi  25560  hmopidmpji  25561  rge0scvg  26384  mblfinlem2  28434  ismtyhmeolem  28708  nacsfix  29053  fnwe2lem2  29409  climinf  29784