Theorem ralrn 7031

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∀wral 3049  ∃wrex 3058  Vcvv 3438  ran crn 5623   Fn wfn 6485  ‘cfv 6490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-iota 6446  df-fun 6492  df-fn 6493  df-fv 6498

This theorem is referenced by:  ralrnmptw  7037  ralrnmpt  7039  cbvfo  7233  isoselem  7285  indexfi  9258  ordtypelem9  9429  ordtypelem10  9430  wemapwe  9604  numacn  9957  acndom  9959  rpnnen1lem3  12890  fsequb2  13897  limsuple  15399  limsupval2  15401  climsup  15591  ruclem11  16163  ruclem12  16164  prmreclem6  16847  imasaddfnlem  17447  imasvscafn  17456  cycsubgcl  19133  ghmrn  19156  ghmnsgima  19167  pgpssslw  19541  gexex  19780  dprdfcntz  19944  znf1o  21504  frlmlbs  21750  lindfrn  21774  ptcnplem  23563  kqt0lem  23678  isr0  23679  regr1lem2  23682  uzrest  23839  tmdgsum2  24038  imasf1oxmet  24317  imasf1omet  24318  bndth  24911  evth  24912  ovolficcss  25424  ovollb2lem  25443  ovolunlem1  25452  ovoliunlem1  25457  ovoliunlem2  25458  ovoliun2  25461  ovolscalem1  25468  ovolicc1  25471  voliunlem2  25506  voliunlem3  25507  ioombl1lem4  25516  uniioovol  25534  uniioombllem2  25538  uniioombllem3  25540  uniioombllem6  25543  volsup2  25560  vitalilem3  25565  mbfsup  25619  mbfinf  25620  mbflimsup  25621  itg1ge0  25641  itg1mulc  25659  itg1climres  25669  mbfi1fseqlem4  25673  itg2seq  25697  itg2monolem1  25705  itg2mono  25708  itg2i1fseq2  25711  itg2gt0  25715  itg2cnlem1  25716  itg2cn  25718  limciun  25849  plycpn  26251  hmopidmchi  32175  hmopidmpji  32176  rge0scvg  34055  mclsax  35712  mblfinlem2  37798  ismtyhmeolem  37944  nacsfix  42896  fnwe2lem2  43235  gneispace  44317  climinf  45794  liminfval2  45954