Theorem ralrn 7021

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 6837	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ V)
2		fvelrnb 6882	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥))
3		eqcom 2738	. . . 4 ⊢ ((𝐹‘𝑦) = 𝑥 ↔ 𝑥 = (𝐹‘𝑦))
4	3	rexbii 3079	. . 3 ⊢ (∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦))
5	2, 4	bitrdi 287	. 2 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦)))
6		rexrn.1	. . 3 ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))
7	6	adantl 481	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜑 ↔ 𝜓))
8	1, 5, 7	ralxfr2d 5346	1 ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ∀wral 3047  ∃wrex 3056  Vcvv 3436  ran crn 5615   Fn wfn 6476  ‘cfv 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-iota 6437  df-fun 6483  df-fn 6484  df-fv 6489

This theorem is referenced by:  ralrnmptw  7027  ralrnmpt  7029  cbvfo  7223  isoselem  7275  indexfi  9244  ordtypelem9  9412  ordtypelem10  9413  wemapwe  9587  numacn  9940  acndom  9942  rpnnen1lem3  12877  fsequb2  13883  limsuple  15385  limsupval2  15387  climsup  15577  ruclem11  16149  ruclem12  16150  prmreclem6  16833  imasaddfnlem  17432  imasvscafn  17441  cycsubgcl  19118  ghmrn  19141  ghmnsgima  19152  pgpssslw  19526  gexex  19765  dprdfcntz  19929  znf1o  21488  frlmlbs  21734  lindfrn  21758  ptcnplem  23536  kqt0lem  23651  isr0  23652  regr1lem2  23655  uzrest  23812  tmdgsum2  24011  imasf1oxmet  24290  imasf1omet  24291  bndth  24884  evth  24885  ovolficcss  25397  ovollb2lem  25416  ovolunlem1  25425  ovoliunlem1  25430  ovoliunlem2  25431  ovoliun2  25434  ovolscalem1  25441  ovolicc1  25444  voliunlem2  25479  voliunlem3  25480  ioombl1lem4  25489  uniioovol  25507  uniioombllem2  25511  uniioombllem3  25513  uniioombllem6  25516  volsup2  25533  vitalilem3  25538  mbfsup  25592  mbfinf  25593  mbflimsup  25594  itg1ge0  25614  itg1mulc  25632  itg1climres  25642  mbfi1fseqlem4  25646  itg2seq  25670  itg2monolem1  25678  itg2mono  25681  itg2i1fseq2  25684  itg2gt0  25688  itg2cnlem1  25689  itg2cn  25691  limciun  25822  plycpn  26224  hmopidmchi  32131  hmopidmpji  32132  rge0scvg  33962  mclsax  35613  mblfinlem2  37697  ismtyhmeolem  37843  nacsfix  42804  fnwe2lem2  43143  gneispace  44226  climinf  45705  liminfval2  45865