Theorem ralrn 7044

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062  Vcvv 3442  ran crn 5635   Fn wfn 6497  ‘cfv 6502

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5245  ax-nul 5255  ax-pr 5381

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-iota 6458  df-fun 6504  df-fn 6505  df-fv 6510

This theorem is referenced by:  ralrnmptw  7050  ralrnmpt  7052  cbvfo  7247  isoselem  7299  indexfi  9274  ordtypelem9  9445  ordtypelem10  9446  wemapwe  9620  numacn  9973  acndom  9975  rpnnen1lem3  12906  fsequb2  13913  limsuple  15415  limsupval2  15417  climsup  15607  ruclem11  16179  ruclem12  16180  prmreclem6  16863  imasaddfnlem  17463  imasvscafn  17472  cycsubgcl  19152  ghmrn  19175  ghmnsgima  19186  pgpssslw  19560  gexex  19799  dprdfcntz  19963  znf1o  21523  frlmlbs  21769  lindfrn  21793  ptcnplem  23582  kqt0lem  23697  isr0  23698  regr1lem2  23701  uzrest  23858  tmdgsum2  24057  imasf1oxmet  24336  imasf1omet  24337  bndth  24930  evth  24931  ovolficcss  25443  ovollb2lem  25462  ovolunlem1  25471  ovoliunlem1  25476  ovoliunlem2  25477  ovoliun2  25480  ovolscalem1  25487  ovolicc1  25490  voliunlem2  25525  voliunlem3  25526  ioombl1lem4  25535  uniioovol  25553  uniioombllem2  25557  uniioombllem3  25559  uniioombllem6  25562  volsup2  25579  vitalilem3  25584  mbfsup  25638  mbfinf  25639  mbflimsup  25640  itg1ge0  25660  itg1mulc  25678  itg1climres  25688  mbfi1fseqlem4  25692  itg2seq  25716  itg2monolem1  25724  itg2mono  25727  itg2i1fseq2  25730  itg2gt0  25734  itg2cnlem1  25735  itg2cn  25737  limciun  25868  plycpn  26270  hmopidmchi  32245  hmopidmpji  32246  rge0scvg  34133  mclsax  35791  mblfinlem2  37938  ismtyhmeolem  38084  nacsfix  43098  fnwe2lem2  43437  gneispace  44519  climinf  45995  liminfval2  46155