Theorem ralrn 7088

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 6900	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ V)
2		fvelrnb 6945	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥))
3		eqcom 2768	. . . 4 ⊢ ((𝐹‘𝑦) = 𝑥 ↔ 𝑥 = (𝐹‘𝑦))
4	3	rexbii 3110	. . 3 ⊢ (∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦))
5	2, 4	bitrdi 290	. 2 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦)))
6		rexrn.1	. . 3 ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))
7	6	adantl 487	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜑 ↔ 𝜓))
8	1, 5, 7	ralxfr2d 5372	1 ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3077  ∃wrex 3087  Vcvv 3451  ran crn 5652   Fn wfn 6533  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6494  df-fun 6540  df-fn 6541  df-fv 6546

This theorem is used by:  ralrnmptw  7094  ralrnmpt  7096  cbvfo  7297  isoselem  7349  fnwe2lem3  8147  indexfi  9349  ordtypelem9  9520  ordtypelem10  9521  wemapwe  9698  numacn  10128  acndom  10130  rpnnen1lem3  13107  fsequb2  14119  limsuple  15645  limsupval2  15647  climsup  15837  ruclem11  16408  ruclem12  16409  prmreclem6  17099  imasaddfnlem  17700  imasvscafn  17709  cycsubgcl  19421  ghmrn  19443  ghmnsgima  19454  pgpssslw  19828  gexex  20067  dprdfcntz  20231  znf1o  21857  frlmlbs  22103  lindfrn  22127  ptcnplem  23940  kqt0lem  24055  isr0  24056  regr1lem2  24059  uzrest  24216  tmdgsum2  24415  imasf1oxmet  24694  imasf1omet  24695  bndth  25279  evth  25280  ovolficcss  25790  ovollb2lem  25809  ovolunlem1  25818  ovoliunlem1  25823  ovoliunlem2  25824  ovoliun2  25827  ovolscalem1  25834  ovolicc1  25837  voliunlem2  25872  voliunlem3  25873  ioombl1lem4  25882  uniioovol  25900  uniioombllem2  25904  uniioombllem3  25906  uniioombllem6  25909  volsup2  25926  vitalilem3  25931  mbfsup  25985  mbfinf  25986  mbflimsup  25987  itg1ge0  26007  itg1mulc  26025  itg1climres  26035  mbfi1fseqlem4  26039  itg2seq  26063  itg2monolem1  26071  itg2mono  26074  itg2i1fseq2  26077  itg2gt0  26081  itg2cnlem1  26082  itg2cn  26084  limciun  26214  plycpn  26610  hmopidmchi  32753  hmopidmpji  32754  rge0scvg  34581  mclsax  36334  mblfinlem2  38576  ismtyhmeolem  38738  nacsfix  43722  gneispace  45133  climinf  46617  liminfval2  46777