Theorem ralrn 7090

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 6907	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ V)
2		fvelrnb 6953	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥))
3		eqcom 2737	. . . 4 ⊢ ((𝐹‘𝑦) = 𝑥 ↔ 𝑥 = (𝐹‘𝑦))
4	3	rexbii 3092	. . 3 ⊢ (∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦))
5	2, 4	bitrdi 286	. 2 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦)))
6		rexrn.1	. . 3 ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))
7	6	adantl 480	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜑 ↔ 𝜓))
8	1, 5, 7	ralxfr2d 5409	1 ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539   ∈ wcel 2104  ∀wral 3059  ∃wrex 3068  Vcvv 3472  ran crn 5678   Fn wfn 6539  ‘cfv 6544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-iota 6496  df-fun 6546  df-fn 6547  df-fv 6552

This theorem is referenced by:  ralrnmptw  7096  ralrnmpt  7098  cbvfo  7291  isoselem  7342  indexfi  9364  ordtypelem9  9525  ordtypelem10  9526  wemapwe  9696  numacn  10048  acndom  10050  rpnnen1lem3  12969  fsequb2  13947  limsuple  15428  limsupval2  15430  climsup  15622  ruclem11  16189  ruclem12  16190  prmreclem6  16860  imasaddfnlem  17480  imasvscafn  17489  cycsubgcl  19123  ghmrn  19145  ghmnsgima  19156  pgpssslw  19525  gexex  19764  dprdfcntz  19928  znf1o  21328  frlmlbs  21573  lindfrn  21597  ptcnplem  23347  kqt0lem  23462  isr0  23463  regr1lem2  23466  uzrest  23623  tmdgsum2  23822  imasf1oxmet  24103  imasf1omet  24104  bndth  24706  evth  24707  ovolficcss  25220  ovollb2lem  25239  ovolunlem1  25248  ovoliunlem1  25253  ovoliunlem2  25254  ovoliun2  25257  ovolscalem1  25264  ovolicc1  25267  voliunlem2  25302  voliunlem3  25303  ioombl1lem4  25312  uniioovol  25330  uniioombllem2  25334  uniioombllem3  25336  uniioombllem6  25339  volsup2  25356  vitalilem3  25361  mbfsup  25415  mbfinf  25416  mbflimsup  25417  itg1ge0  25437  itg1mulc  25456  itg1climres  25466  mbfi1fseqlem4  25470  itg2seq  25494  itg2monolem1  25502  itg2mono  25505  itg2i1fseq2  25508  itg2gt0  25512  itg2cnlem1  25513  itg2cn  25515  limciun  25645  plycpn  26036  hmopidmchi  31669  hmopidmpji  31670  rge0scvg  33225  mclsax  34856  mblfinlem2  36831  ismtyhmeolem  36977  nacsfix  41754  fnwe2lem2  42097  gneispace  43189  climinf  44622  liminfval2  44784