Theorem ralrn 6840

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 6671	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ V)
2		fvelrnb 6712	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥))
3		eqcom 2828	. . . 4 ⊢ ((𝐹‘𝑦) = 𝑥 ↔ 𝑥 = (𝐹‘𝑦))
4	3	rexbii 3247	. . 3 ⊢ (∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦))
5	2, 4	syl6bb 289	. 2 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦)))
6		rexrn.1	. . 3 ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))
7	6	adantl 484	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜑 ↔ 𝜓))
8	1, 5, 7	ralxfr2d 5297	1 ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∀wral 3138  ∃wrex 3139  Vcvv 3486  ran crn 5542   Fn wfn 6336  ‘cfv 6341

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5189  ax-nul 5196  ax-pr 5316

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3488  df-sbc 3764  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-nul 4280  df-if 4454  df-sn 4554  df-pr 4556  df-op 4560  df-uni 4825  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5446  df-xp 5547  df-rel 5548  df-cnv 5549  df-co 5550  df-dm 5551  df-rn 5552  df-iota 6300  df-fun 6343  df-fn 6344  df-fv 6349

This theorem is referenced by:  ralrnmptw  6846  ralrnmpt  6848  cbvfo  7031  isoselem  7080  indexfi  8818  ordtypelem9  8976  ordtypelem10  8977  wemapwe  9146  numacn  9461  acndom  9463  rpnnen1lem3  12365  fsequb2  13334  limsuple  14820  limsupval2  14822  climsup  15011  ruclem11  15578  ruclem12  15579  prmreclem6  16240  imasaddfnlem  16784  imasvscafn  16793  cycsubgcl  18332  ghmrn  18354  ghmnsgima  18365  pgpssslw  18722  gexex  18956  dprdfcntz  19120  znf1o  20681  frlmlbs  20924  lindfrn  20948  ptcnplem  22212  kqt0lem  22327  isr0  22328  regr1lem2  22331  uzrest  22488  tmdgsum2  22687  imasf1oxmet  22968  imasf1omet  22969  bndth  23545  evth  23546  ovolficcss  24053  ovollb2lem  24072  ovolunlem1  24081  ovoliunlem1  24086  ovoliunlem2  24087  ovoliun2  24090  ovolscalem1  24097  ovolicc1  24100  voliunlem2  24135  voliunlem3  24136  ioombl1lem4  24145  uniioovol  24163  uniioombllem2  24167  uniioombllem3  24169  uniioombllem6  24172  volsup2  24189  vitalilem3  24194  mbfsup  24248  mbfinf  24249  mbflimsup  24250  itg1ge0  24270  itg1mulc  24288  itg1climres  24298  mbfi1fseqlem4  24302  itg2seq  24326  itg2monolem1  24334  itg2mono  24337  itg2i1fseq2  24340  itg2gt0  24344  itg2cnlem1  24345  itg2cn  24347  limciun  24477  plycpn  24864  hmopidmchi  29912  hmopidmpji  29913  rge0scvg  31199  mclsax  32823  mblfinlem2  34964  ismtyhmeolem  35114  nacsfix  39401  fnwe2lem2  39743  gneispace  40574  climinf  41977  liminfval2  42139