Theorem ralrn 6946

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 6771	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ V)
2		fvelrnb 6812	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥))
3		eqcom 2745	. . . 4 ⊢ ((𝐹‘𝑦) = 𝑥 ↔ 𝑥 = (𝐹‘𝑦))
4	3	rexbii 3177	. . 3 ⊢ (∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦))
5	2, 4	bitrdi 286	. 2 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦)))
6		rexrn.1	. . 3 ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))
7	6	adantl 481	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜑 ↔ 𝜓))
8	1, 5, 7	ralxfr2d 5328	1 ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ∀wral 3063  ∃wrex 3064  Vcvv 3422  ran crn 5581   Fn wfn 6413  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-iota 6376  df-fun 6420  df-fn 6421  df-fv 6426

This theorem is referenced by:  ralrnmptw  6952  ralrnmpt  6954  cbvfo  7141  isoselem  7192  indexfi  9057  ordtypelem9  9215  ordtypelem10  9216  wemapwe  9385  numacn  9736  acndom  9738  rpnnen1lem3  12648  fsequb2  13624  limsuple  15115  limsupval2  15117  climsup  15309  ruclem11  15877  ruclem12  15878  prmreclem6  16550  imasaddfnlem  17156  imasvscafn  17165  cycsubgcl  18740  ghmrn  18762  ghmnsgima  18773  pgpssslw  19134  gexex  19369  dprdfcntz  19533  znf1o  20671  frlmlbs  20914  lindfrn  20938  ptcnplem  22680  kqt0lem  22795  isr0  22796  regr1lem2  22799  uzrest  22956  tmdgsum2  23155  imasf1oxmet  23436  imasf1omet  23437  bndth  24027  evth  24028  ovolficcss  24538  ovollb2lem  24557  ovolunlem1  24566  ovoliunlem1  24571  ovoliunlem2  24572  ovoliun2  24575  ovolscalem1  24582  ovolicc1  24585  voliunlem2  24620  voliunlem3  24621  ioombl1lem4  24630  uniioovol  24648  uniioombllem2  24652  uniioombllem3  24654  uniioombllem6  24657  volsup2  24674  vitalilem3  24679  mbfsup  24733  mbfinf  24734  mbflimsup  24735  itg1ge0  24755  itg1mulc  24774  itg1climres  24784  mbfi1fseqlem4  24788  itg2seq  24812  itg2monolem1  24820  itg2mono  24823  itg2i1fseq2  24826  itg2gt0  24830  itg2cnlem1  24831  itg2cn  24833  limciun  24963  plycpn  25354  hmopidmchi  30414  hmopidmpji  30415  rge0scvg  31801  mclsax  33431  mblfinlem2  35742  ismtyhmeolem  35889  nacsfix  40450  fnwe2lem2  40792  gneispace  41633  climinf  43037  liminfval2  43199