Theorem ralrn 7082

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3076  ∃wrex 3086  Vcvv 3450  ran crn 5656   Fn wfn 6528  ‘cfv 6533

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 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6489  df-fun 6535  df-fn 6536  df-fv 6541

This theorem is used by:  ralrnmptw  7088  ralrnmpt  7090  cbvfo  7291  isoselem  7343  indexfi  9330  ordtypelem9  9501  ordtypelem10  9502  wemapwe  9679  numacn  10055  acndom  10057  rpnnen1lem3  13032  fsequb2  14043  limsuple  15568  limsupval2  15570  climsup  15760  ruclem11  16331  ruclem12  16332  prmreclem6  17016  imasaddfnlem  17617  imasvscafn  17626  cycsubgcl  19337  ghmrn  19359  ghmnsgima  19370  pgpssslw  19744  gexex  19983  dprdfcntz  20147  znf1o  21767  frlmlbs  22013  lindfrn  22037  ptcnplem  23850  kqt0lem  23965  isr0  23966  regr1lem2  23969  uzrest  24126  tmdgsum2  24325  imasf1oxmet  24604  imasf1omet  24605  bndth  25189  evth  25190  ovolficcss  25700  ovollb2lem  25719  ovolunlem1  25728  ovoliunlem1  25733  ovoliunlem2  25734  ovoliun2  25737  ovolscalem1  25744  ovolicc1  25747  voliunlem2  25782  voliunlem3  25783  ioombl1lem4  25792  uniioovol  25810  uniioombllem2  25814  uniioombllem3  25816  uniioombllem6  25819  volsup2  25836  vitalilem3  25841  mbfsup  25895  mbfinf  25896  mbflimsup  25897  itg1ge0  25917  itg1mulc  25935  itg1climres  25945  mbfi1fseqlem4  25949  itg2seq  25973  itg2monolem1  25981  itg2mono  25984  itg2i1fseq2  25987  itg2gt0  25991  itg2cnlem1  25992  itg2cn  25994  limciun  26124  plycpn  26522  hmopidmchi  32635  hmopidmpji  32636  rge0scvg  34462  mclsax  36151  mblfinlem2  38410  ismtyhmeolem  38557  nacsfix  43560  fnwe2lem2  43895  gneispace  44977  climinf  46439  liminfval2  46599