Theorem ralrn 6719

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 6553	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ V)
2		fvelrnb 6594	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥))
3		eqcom 2802	. . . 4 ⊢ ((𝐹‘𝑦) = 𝑥 ↔ 𝑥 = (𝐹‘𝑦))
4	3	rexbii 3211	. . 3 ⊢ (∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦))
5	2, 4	syl6bb 288	. 2 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦)))
6		rexrn.1	. . 3 ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))
7	6	adantl 482	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜑 ↔ 𝜓))
8	1, 5, 7	ralxfr2d 5202	1 ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1522   ∈ wcel 2081  ∀wral 3105  ∃wrex 3106  Vcvv 3437  ran crn 5444   Fn wfn 6220  ‘cfv 6225

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pr 5221

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-opab 5025  df-mpt 5042  df-id 5348  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-iota 6189  df-fun 6227  df-fn 6228  df-fv 6233

This theorem is referenced by:  ralrnmpt  6725  cbvfo  6910  isoselem  6957  indexfi  8678  ordtypelem9  8836  ordtypelem10  8837  wemapwe  9006  numacn  9321  acndom  9323  rpnnen1lem3  12228  fsequb2  13194  limsuple  14669  limsupval2  14671  climsup  14860  ruclem11  15426  ruclem12  15427  prmreclem6  16086  imasaddfnlem  16630  imasvscafn  16639  cycsubgcl  18059  ghmrn  18112  ghmnsgima  18123  pgpssslw  18469  gexex  18696  dprdfcntz  18854  znf1o  20380  frlmlbs  20623  lindfrn  20647  ptcnplem  21913  kqt0lem  22028  isr0  22029  regr1lem2  22032  uzrest  22189  tmdgsum2  22388  imasf1oxmet  22668  imasf1omet  22669  bndth  23245  evth  23246  ovolficcss  23753  ovollb2lem  23772  ovolunlem1  23781  ovoliunlem1  23786  ovoliunlem2  23787  ovoliun2  23790  ovolscalem1  23797  ovolicc1  23800  voliunlem2  23835  voliunlem3  23836  ioombl1lem4  23845  uniioovol  23863  uniioombllem2  23867  uniioombllem3  23869  uniioombllem6  23872  volsup2  23889  vitalilem3  23894  mbfsup  23948  mbfinf  23949  mbflimsup  23950  itg1ge0  23970  itg1mulc  23988  itg1climres  23998  mbfi1fseqlem4  24002  itg2seq  24026  itg2monolem1  24034  itg2mono  24037  itg2i1fseq2  24040  itg2gt0  24044  itg2cnlem1  24045  itg2cn  24047  limciun  24175  plycpn  24561  hmopidmchi  29619  hmopidmpji  29620  rge0scvg  30809  mclsax  32424  mblfinlem2  34461  ismtyhmeolem  34614  nacsfix  38794  fnwe2lem2  39136  gneispace  39969  climinf  41429  liminfval2  41591