Theorem ralrn 7108

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 6922	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ V)
2		fvelrnb 6969	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥))
3		eqcom 2742	. . . 4 ⊢ ((𝐹‘𝑦) = 𝑥 ↔ 𝑥 = (𝐹‘𝑦))
4	3	rexbii 3092	. . 3 ⊢ (∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦))
5	2, 4	bitrdi 287	. 2 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦)))
6		rexrn.1	. . 3 ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))
7	6	adantl 481	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜑 ↔ 𝜓))
8	1, 5, 7	ralxfr2d 5416	1 ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2106  ∀wral 3059  ∃wrex 3068  Vcvv 3478  ran crn 5690   Fn wfn 6558  ‘cfv 6563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-iota 6516  df-fun 6565  df-fn 6566  df-fv 6571

This theorem is referenced by:  ralrnmptw  7114  ralrnmpt  7116  cbvfo  7309  isoselem  7361  indexfi  9398  ordtypelem9  9564  ordtypelem10  9565  wemapwe  9735  numacn  10087  acndom  10089  rpnnen1lem3  13019  fsequb2  14014  limsuple  15511  limsupval2  15513  climsup  15703  ruclem11  16273  ruclem12  16274  prmreclem6  16955  imasaddfnlem  17575  imasvscafn  17584  cycsubgcl  19237  ghmrn  19260  ghmnsgima  19271  pgpssslw  19647  gexex  19886  dprdfcntz  20050  znf1o  21588  frlmlbs  21835  lindfrn  21859  ptcnplem  23645  kqt0lem  23760  isr0  23761  regr1lem2  23764  uzrest  23921  tmdgsum2  24120  imasf1oxmet  24401  imasf1omet  24402  bndth  25004  evth  25005  ovolficcss  25518  ovollb2lem  25537  ovolunlem1  25546  ovoliunlem1  25551  ovoliunlem2  25552  ovoliun2  25555  ovolscalem1  25562  ovolicc1  25565  voliunlem2  25600  voliunlem3  25601  ioombl1lem4  25610  uniioovol  25628  uniioombllem2  25632  uniioombllem3  25634  uniioombllem6  25637  volsup2  25654  vitalilem3  25659  mbfsup  25713  mbfinf  25714  mbflimsup  25715  itg1ge0  25735  itg1mulc  25754  itg1climres  25764  mbfi1fseqlem4  25768  itg2seq  25792  itg2monolem1  25800  itg2mono  25803  itg2i1fseq2  25806  itg2gt0  25810  itg2cnlem1  25811  itg2cn  25813  limciun  25944  plycpn  26346  hmopidmchi  32180  hmopidmpji  32181  rge0scvg  33910  mclsax  35554  mblfinlem2  37645  ismtyhmeolem  37791  nacsfix  42700  fnwe2lem2  43040  gneispace  44124  climinf  45562  liminfval2  45724