Theorem ralrn 6270

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		fvex 6113	. . 3 ⊢ (𝐹‘𝑦) ∈ V
2	1	a1i 11	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ V)
3		fvelrnb 6153	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥))
4		eqcom 2617	. . . 4 ⊢ ((𝐹‘𝑦) = 𝑥 ↔ 𝑥 = (𝐹‘𝑦))
5	4	rexbii 3023	. . 3 ⊢ (∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦))
6	3, 5	syl6bb 275	. 2 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦)))
7		rexrn.1	. . 3 ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))
8	7	adantl 481	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜑 ↔ 𝜓))
9	2, 6, 8	ralxfr2d 4808	1 ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897  Vcvv 3173  ran crn 5039   Fn wfn 5799  ‘cfv 5804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-iota 5768  df-fun 5806  df-fn 5807  df-fv 5812

This theorem is referenced by:  ralrnmpt  6276  cbvfo  6444  isoselem  6491  indexfi  8157  ordtypelem9  8314  ordtypelem10  8315  wemapwe  8477  numacn  8755  acndom  8757  rpnnen1lem3  11692  rpnnen1lem3OLD  11698  fsequb2  12637  limsuple  14057  limsupval2  14059  climsup  14248  ruclem11  14808  ruclem12  14809  prmreclem6  15463  imasaddfnlem  16011  imasvscafn  16020  cycsubgcl  17443  ghmrn  17496  ghmnsgima  17507  pgpssslw  17852  gexex  18079  dprdfcntz  18237  znf1o  19719  frlmlbs  19955  lindfrn  19979  ptcnplem  21234  kqt0lem  21349  isr0  21350  regr1lem2  21353  uzrest  21511  tmdgsum2  21710  imasf1oxmet  21990  imasf1omet  21991  bndth  22565  evth  22566  ovolficcss  23045  ovollb2lem  23063  ovolunlem1  23072  ovoliunlem1  23077  ovoliunlem2  23078  ovoliun2  23081  ovolscalem1  23088  ovolicc1  23091  voliunlem2  23126  voliunlem3  23127  ioombl1lem4  23136  uniioovol  23153  uniioombllem2  23157  uniioombllem3  23159  uniioombllem6  23162  volsup2  23179  vitalilem3  23185  mbfsup  23237  mbfinf  23238  mbflimsup  23239  itg1ge0  23259  itg1mulc  23277  itg1climres  23287  mbfi1fseqlem4  23291  itg2seq  23315  itg2monolem1  23323  itg2mono  23326  itg2i1fseq2  23329  itg2gt0  23333  itg2cnlem1  23334  itg2cn  23336  limciun  23464  plycpn  23848  hmopidmchi  28394  hmopidmpji  28395  rge0scvg  29323  mclsax  30720  mblfinlem2  32617  ismtyhmeolem  32773  nacsfix  36293  fnwe2lem2  36639  gneispace  37452  climinf  38673