Theorem ralrn 6362

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		fvexd 6203	. 2 |- ( ( F Fn A /\ y e. A ) -> ( F ` y ) e. _V )
2		fvelrnb 6243	. . 3 |- ( F Fn A -> ( x e. ran F <-> E. y e. A ( F ` y ) = x ) )
3		eqcom 2629	. . . 4 |- ( ( F ` y ) = x <-> x = ( F ` y ) )
4	3	rexbii 3041	. . 3 |- ( E. y e. A ( F ` y ) = x <-> E. y e. A x = ( F ` y ) )
5	2, 4	syl6bb 276	. 2 |- ( F Fn A -> ( x e. ran F <-> E. y e. A x = ( F ` y ) ) )
6		rexrn.1	. . 3 |- ( x = ( F ` y ) -> ( ph <-> ps ) )
7	6	adantl 482	. 2 |- ( ( F Fn A /\ x = ( F ` y ) ) -> ( ph <-> ps ) )
8	1, 5, 7	ralxfr2d 4882	1 |- ( F Fn A -> ( A. x e. ran F ph <-> A. y e. A ps ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912   E.wrex 2913   _Vcvv 3200   ran crn 5115   Fn wfn 5883   ` cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-iota 5851  df-fun 5890  df-fn 5891  df-fv 5896

This theorem is referenced by:  ralrnmpt  6368  cbvfo  6544  isoselem  6591  indexfi  8274  ordtypelem9  8431  ordtypelem10  8432  wemapwe  8594  numacn  8872  acndom  8874  rpnnen1lem3  11816  rpnnen1lem3OLD  11822  fsequb2  12775  limsuple  14209  limsupval2  14211  climsup  14400  ruclem11  14969  ruclem12  14970  prmreclem6  15625  imasaddfnlem  16188  imasvscafn  16197  cycsubgcl  17620  ghmrn  17673  ghmnsgima  17684  pgpssslw  18029  gexex  18256  dprdfcntz  18414  znf1o  19900  frlmlbs  20136  lindfrn  20160  ptcnplem  21424  kqt0lem  21539  isr0  21540  regr1lem2  21543  uzrest  21701  tmdgsum2  21900  imasf1oxmet  22180  imasf1omet  22181  bndth  22757  evth  22758  ovolficcss  23238  ovollb2lem  23256  ovolunlem1  23265  ovoliunlem1  23270  ovoliunlem2  23271  ovoliun2  23274  ovolscalem1  23281  ovolicc1  23284  voliunlem2  23319  voliunlem3  23320  ioombl1lem4  23329  uniioovol  23347  uniioombllem2  23351  uniioombllem3  23353  uniioombllem6  23356  volsup2  23373  vitalilem3  23379  mbfsup  23431  mbfinf  23432  mbflimsup  23433  itg1ge0  23453  itg1mulc  23471  itg1climres  23481  mbfi1fseqlem4  23485  itg2seq  23509  itg2monolem1  23517  itg2mono  23520  itg2i1fseq2  23523  itg2gt0  23527  itg2cnlem1  23528  itg2cn  23530  limciun  23658  plycpn  24044  hmopidmchi  29010  hmopidmpji  29011  rge0scvg  29995  mclsax  31466  mblfinlem2  33447  ismtyhmeolem  33603  nacsfix  37275  fnwe2lem2  37621  gneispace  38432  climinf  39838  liminfval2  40000