Theorem ralrn 6402

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 6241	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ V)
2		fvelrnb 6282	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥))
3		eqcom 2658	. . . 4 ⊢ ((𝐹‘𝑦) = 𝑥 ↔ 𝑥 = (𝐹‘𝑦))
4	3	rexbii 3070	. . 3 ⊢ (∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦))
5	2, 4	syl6bb 276	. 2 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦)))
6		rexrn.1	. . 3 ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))
7	6	adantl 481	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜑 ↔ 𝜓))
8	1, 5, 7	ralxfr2d 4912	1 ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523   ∈ wcel 2030  ∀wral 2941  ∃wrex 2942  Vcvv 3231  ran crn 5144   Fn wfn 5921  ‘cfv 5926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-iota 5889  df-fun 5928  df-fn 5929  df-fv 5934

This theorem is referenced by:  ralrnmpt  6408  cbvfo  6584  isoselem  6631  indexfi  8315  ordtypelem9  8472  ordtypelem10  8473  wemapwe  8632  numacn  8910  acndom  8912  rpnnen1lem3  11854  rpnnen1lem3OLD  11860  fsequb2  12815  limsuple  14253  limsupval2  14255  climsup  14444  ruclem11  15013  ruclem12  15014  prmreclem6  15672  imasaddfnlem  16235  imasvscafn  16244  cycsubgcl  17667  ghmrn  17720  ghmnsgima  17731  pgpssslw  18075  gexex  18302  dprdfcntz  18460  znf1o  19948  frlmlbs  20184  lindfrn  20208  ptcnplem  21472  kqt0lem  21587  isr0  21588  regr1lem2  21591  uzrest  21748  tmdgsum2  21947  imasf1oxmet  22227  imasf1omet  22228  bndth  22804  evth  22805  ovolficcss  23284  ovollb2lem  23302  ovolunlem1  23311  ovoliunlem1  23316  ovoliunlem2  23317  ovoliun2  23320  ovolscalem1  23327  ovolicc1  23330  voliunlem2  23365  voliunlem3  23366  ioombl1lem4  23375  uniioovol  23393  uniioombllem2  23397  uniioombllem3  23399  uniioombllem6  23402  volsup2  23419  vitalilem3  23424  mbfsup  23476  mbfinf  23477  mbflimsup  23478  itg1ge0  23498  itg1mulc  23516  itg1climres  23526  mbfi1fseqlem4  23530  itg2seq  23554  itg2monolem1  23562  itg2mono  23565  itg2i1fseq2  23568  itg2gt0  23572  itg2cnlem1  23573  itg2cn  23575  limciun  23703  plycpn  24089  hmopidmchi  29138  hmopidmpji  29139  rge0scvg  30123  mclsax  31592  mblfinlem2  33577  ismtyhmeolem  33733  nacsfix  37592  fnwe2lem2  37938  gneispace  38749  climinf  40156  liminfval2  40318