Theorem ralrn 6845

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 6673	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ V)
2		fvelrnb 6714	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥))
3		eqcom 2765	. . . 4 ⊢ ((𝐹‘𝑦) = 𝑥 ↔ 𝑥 = (𝐹‘𝑦))
4	3	rexbii 3175	. . 3 ⊢ (∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦))
5	2, 4	bitrdi 290	. 2 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦)))
6		rexrn.1	. . 3 ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))
7	6	adantl 485	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜑 ↔ 𝜓))
8	1, 5, 7	ralxfr2d 5279	1 ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3070  ∃wrex 3071  Vcvv 3409  ran crn 5525   Fn wfn 6330  ‘cfv 6335

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ral 3075  df-rex 3076  df-v 3411  df-sbc 3697  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-iota 6294  df-fun 6337  df-fn 6338  df-fv 6343

This theorem is referenced by:  ralrnmptw  6851  ralrnmpt  6853  cbvfo  7037  isoselem  7088  indexfi  8865  ordtypelem9  9023  ordtypelem10  9024  wemapwe  9193  numacn  9509  acndom  9511  rpnnen1lem3  12419  fsequb2  13393  limsuple  14883  limsupval2  14885  climsup  15074  ruclem11  15641  ruclem12  15642  prmreclem6  16312  imasaddfnlem  16859  imasvscafn  16868  cycsubgcl  18416  ghmrn  18438  ghmnsgima  18449  pgpssslw  18806  gexex  19041  dprdfcntz  19205  znf1o  20319  frlmlbs  20562  lindfrn  20586  ptcnplem  22321  kqt0lem  22436  isr0  22437  regr1lem2  22440  uzrest  22597  tmdgsum2  22796  imasf1oxmet  23077  imasf1omet  23078  bndth  23659  evth  23660  ovolficcss  24169  ovollb2lem  24188  ovolunlem1  24197  ovoliunlem1  24202  ovoliunlem2  24203  ovoliun2  24206  ovolscalem1  24213  ovolicc1  24216  voliunlem2  24251  voliunlem3  24252  ioombl1lem4  24261  uniioovol  24279  uniioombllem2  24283  uniioombllem3  24285  uniioombllem6  24288  volsup2  24305  vitalilem3  24310  mbfsup  24364  mbfinf  24365  mbflimsup  24366  itg1ge0  24386  itg1mulc  24404  itg1climres  24414  mbfi1fseqlem4  24418  itg2seq  24442  itg2monolem1  24450  itg2mono  24453  itg2i1fseq2  24456  itg2gt0  24460  itg2cnlem1  24461  itg2cn  24463  limciun  24593  plycpn  24984  hmopidmchi  30033  hmopidmpji  30034  rge0scvg  31420  mclsax  33047  mblfinlem2  35397  ismtyhmeolem  35544  nacsfix  40048  fnwe2lem2  40390  gneispace  41232  climinf  42636  liminfval2  42798