Theorem ralrn 7085

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3078  ∃wrex 3088  Vcvv 3453  ran crn 5660   Fn wfn 6532  ‘cfv 6537

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 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-iota 6493  df-fun 6539  df-fn 6540  df-fv 6545

This theorem is used by:  ralrnmptw  7091  ralrnmpt  7093  cbvfo  7294  isoselem  7346  indexfi  9331  ordtypelem9  9502  ordtypelem10  9503  wemapwe  9680  numacn  10056  acndom  10058  rpnnen1lem3  13033  fsequb2  14044  limsuple  15569  limsupval2  15571  climsup  15761  ruclem11  16334  ruclem12  16335  prmreclem6  17019  imasaddfnlem  17620  imasvscafn  17629  cycsubgcl  19340  ghmrn  19362  ghmnsgima  19373  pgpssslw  19747  gexex  19986  dprdfcntz  20150  znf1o  21770  frlmlbs  22016  lindfrn  22040  ptcnplem  23853  kqt0lem  23968  isr0  23969  regr1lem2  23972  uzrest  24129  tmdgsum2  24328  imasf1oxmet  24607  imasf1omet  24608  bndth  25192  evth  25193  ovolficcss  25703  ovollb2lem  25722  ovolunlem1  25731  ovoliunlem1  25736  ovoliunlem2  25737  ovoliun2  25740  ovolscalem1  25747  ovolicc1  25750  voliunlem2  25785  voliunlem3  25786  ioombl1lem4  25795  uniioovol  25813  uniioombllem2  25817  uniioombllem3  25819  uniioombllem6  25822  volsup2  25839  vitalilem3  25844  mbfsup  25898  mbfinf  25899  mbflimsup  25900  itg1ge0  25920  itg1mulc  25938  itg1climres  25948  mbfi1fseqlem4  25952  itg2seq  25976  itg2monolem1  25984  itg2mono  25987  itg2i1fseq2  25990  itg2gt0  25994  itg2cnlem1  25995  itg2cn  25997  limciun  26128  plycpn  26526  hmopidmchi  32640  hmopidmpji  32641  rge0scvg  34467  mclsax  36156  mblfinlem2  38415  ismtyhmeolem  38562  nacsfix  43565  fnwe2lem2  43900  gneispace  44982  climinf  46444  liminfval2  46604