Theorem ralrn 7087

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ∀wral 3081  ∃wrex 3091  Vcvv 3457  ran crn 5664   Fn wfn 6535  ‘cfv 6540

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-iota 6496  df-fun 6542  df-fn 6543  df-fv 6548

This theorem is used by:  ralrnmptw  7093  ralrnmpt  7095  cbvfo  7296  isoselem  7348  indexfi  9324  ordtypelem9  9495  ordtypelem10  9496  wemapwe  9673  numacn  10049  acndom  10051  rpnnen1lem3  13023  fsequb2  14034  limsuple  15557  limsupval2  15559  climsup  15749  ruclem11  16322  ruclem12  16323  prmreclem6  17007  imasaddfnlem  17608  imasvscafn  17617  cycsubgcl  19325  ghmrn  19347  ghmnsgima  19358  pgpssslw  19732  gexex  19971  dprdfcntz  20135  znf1o  21755  frlmlbs  22001  lindfrn  22025  ptcnplem  23833  kqt0lem  23948  isr0  23949  regr1lem2  23952  uzrest  24109  tmdgsum2  24308  imasf1oxmet  24587  imasf1omet  24588  bndth  25172  evth  25173  ovolficcss  25683  ovollb2lem  25702  ovolunlem1  25711  ovoliunlem1  25716  ovoliunlem2  25717  ovoliun2  25720  ovolscalem1  25727  ovolicc1  25730  voliunlem2  25765  voliunlem3  25766  ioombl1lem4  25775  uniioovol  25793  uniioombllem2  25797  uniioombllem3  25799  uniioombllem6  25802  volsup2  25819  vitalilem3  25824  mbfsup  25878  mbfinf  25879  mbflimsup  25880  itg1ge0  25900  itg1mulc  25918  itg1climres  25928  mbfi1fseqlem4  25932  itg2seq  25956  itg2monolem1  25964  itg2mono  25967  itg2i1fseq2  25970  itg2gt0  25974  itg2cnlem1  25975  itg2cn  25977  limciun  26108  plycpn  26505  hmopidmchi  32578  hmopidmpji  32579  rge0scvg  34407  mclsax  36102  mblfinlem2  38370  ismtyhmeolem  38517  nacsfix  43520  fnwe2lem2  43855  gneispace  44937  climinf  46399  liminfval2  46559