Theorem ralrn 7084

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 6897	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ V)
2		fvelrnb 6942	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥))
3		eqcom 2776	. . . 4 ⊢ ((𝐹‘𝑦) = 𝑥 ↔ 𝑥 = (𝐹‘𝑦))
4	3	rexbii 3118	. . 3 ⊢ (∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦))
5	2, 4	bitrdi 290	. 2 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦)))
6		rexrn.1	. . 3 ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))
7	6	adantl 486	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜑 ↔ 𝜓))
8	1, 5, 7	ralxfr2d 5382	1 ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∀wral 3085  ∃wrex 3095  Vcvv 3463  ran crn 5663   Fn wfn 6532  ‘cfv 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-iota 6493  df-fun 6539  df-fn 6540  df-fv 6545

This theorem is referenced by:  ralrnmptw  7090  ralrnmpt  7092  cbvfo  7288  isoselem  7340  indexfi  9317  ordtypelem9  9488  ordtypelem10  9489  wemapwe  9666  numacn  10033  acndom  10035  rpnnen1lem3  13003  fsequb2  14012  limsuple  15529  limsupval2  15531  climsup  15721  ruclem11  16296  ruclem12  16297  prmreclem6  16981  imasaddfnlem  17582  imasvscafn  17591  cycsubgcl  19277  ghmrn  19299  ghmnsgima  19310  pgpssslw  19684  gexex  19923  dprdfcntz  20087  znf1o  21670  frlmlbs  21916  lindfrn  21940  ptcnplem  23747  kqt0lem  23862  isr0  23863  regr1lem2  23866  uzrest  24023  tmdgsum2  24222  imasf1oxmet  24501  imasf1omet  24502  bndth  25086  evth  25087  ovolficcss  25597  ovollb2lem  25616  ovolunlem1  25625  ovoliunlem1  25630  ovoliunlem2  25631  ovoliun2  25634  ovolscalem1  25641  ovolicc1  25644  voliunlem2  25679  voliunlem3  25680  ioombl1lem4  25689  uniioovol  25707  uniioombllem2  25711  uniioombllem3  25713  uniioombllem6  25716  volsup2  25733  vitalilem3  25738  mbfsup  25792  mbfinf  25793  mbflimsup  25794  itg1ge0  25814  itg1mulc  25832  itg1climres  25842  mbfi1fseqlem4  25846  itg2seq  25870  itg2monolem1  25878  itg2mono  25881  itg2i1fseq2  25884  itg2gt0  25888  itg2cnlem1  25889  itg2cn  25891  limciun  26022  plycpn  26419  hmopidmchi  32444  hmopidmpji  32445  rge0scvg  34284  mclsax  35994  mblfinlem2  38231  ismtyhmeolem  38377  nacsfix  43369  fnwe2lem2  43704  gneispace  44786  climinf  46248  liminfval2  46408