Theorem ralrn 7071

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	⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
ralrn	⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐹,𝑦   𝜓,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem ralrn

Step	Hyp	Ref	Expression
1		fvexd 6884	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ V)
2		fvelrnb 6929	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥))
3		eqcom 2771	. . . 4 ⊢ ((𝐹‘𝑦) = 𝑥 ↔ 𝑥 = (𝐹‘𝑦))
4	3	rexbii 3111	. . 3 ⊢ (∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦))
5	2, 4	bitrdi 289	. 2 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦)))
6		rexrn.1	. . 3 ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))
7	6	adantl 485	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜑 ↔ 𝜓))
8	1, 5, 7	ralxfr2d 5369	1 ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1562   ∈ wcel 2144  ∀wral 3078  ∃wrex 3088  Vcvv 3456  ran crn 5650   Fn wfn 6518  ‘cfv 6523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-sep 5248  ax-nul 5258  ax-pr 5392

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5544  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-iota 6479  df-fun 6525  df-fn 6526  df-fv 6531

This theorem is referenced by:  ralrnmptw  7077  ralrnmpt  7079  cbvfo  7275  isoselem  7327  indexfi  9305  ordtypelem9  9476  ordtypelem10  9477  wemapwe  9654  numacn  10007  acndom  10009  rpnnen1lem3  12982  fsequb2  13991  limsuple  15507  limsupval2  15509  climsup  15699  ruclem11  16274  ruclem12  16275  prmreclem6  16959  imasaddfnlem  17560  imasvscafn  17569  cycsubgcl  19249  ghmrn  19271  ghmnsgima  19282  pgpssslw  19656  gexex  19895  dprdfcntz  20059  znf1o  21605  frlmlbs  21851  lindfrn  21875  ptcnplem  23683  kqt0lem  23798  isr0  23799  regr1lem2  23802  uzrest  23959  tmdgsum2  24158  imasf1oxmet  24437  imasf1omet  24438  bndth  25022  evth  25023  ovolficcss  25533  ovollb2lem  25552  ovolunlem1  25561  ovoliunlem1  25566  ovoliunlem2  25567  ovoliun2  25570  ovolscalem1  25577  ovolicc1  25580  voliunlem2  25615  voliunlem3  25616  ioombl1lem4  25625  uniioovol  25643  uniioombllem2  25647  uniioombllem3  25649  uniioombllem6  25652  volsup2  25669  vitalilem3  25674  mbfsup  25728  mbfinf  25729  mbflimsup  25730  itg1ge0  25750  itg1mulc  25768  itg1climres  25778  mbfi1fseqlem4  25782  itg2seq  25806  itg2monolem1  25814  itg2mono  25817  itg2i1fseq2  25820  itg2gt0  25824  itg2cnlem1  25825  itg2cn  25827  limciun  25958  plycpn  26355  hmopidmchi  32356  hmopidmpji  32357  rge0scvg  34248  mclsax  35924  mblfinlem2  38162  ismtyhmeolem  38308  nacsfix  43298  fnwe2lem2  43633  gneispace  44715  climinf  46187  liminfval2  46347