MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralrn Structured version   Visualization version   GIF version

Theorem ralrn 6319
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
StepHypRef Expression
1 fvex 6160 . . 3 (𝐹𝑦) ∈ V
21a1i 11 . 2 ((𝐹 Fn 𝐴𝑦𝐴) → (𝐹𝑦) ∈ V)
3 fvelrnb 6201 . . 3 (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦𝐴 (𝐹𝑦) = 𝑥))
4 eqcom 2633 . . . 4 ((𝐹𝑦) = 𝑥𝑥 = (𝐹𝑦))
54rexbii 3039 . . 3 (∃𝑦𝐴 (𝐹𝑦) = 𝑥 ↔ ∃𝑦𝐴 𝑥 = (𝐹𝑦))
63, 5syl6bb 276 . 2 (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦𝐴 𝑥 = (𝐹𝑦)))
7 rexrn.1 . . 3 (𝑥 = (𝐹𝑦) → (𝜑𝜓))
87adantl 482 . 2 ((𝐹 Fn 𝐴𝑥 = (𝐹𝑦)) → (𝜑𝜓))
92, 6, 8ralxfr2d 4847 1 (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1992  wral 2912  wrex 2913  Vcvv 3191  ran crn 5080   Fn wfn 5845  cfv 5850
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pr 4872
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-iota 5813  df-fun 5852  df-fn 5853  df-fv 5858
This theorem is referenced by:  ralrnmpt  6325  cbvfo  6499  isoselem  6546  indexfi  8219  ordtypelem9  8376  ordtypelem10  8377  wemapwe  8539  numacn  8817  acndom  8819  rpnnen1lem3  11760  rpnnen1lem3OLD  11766  fsequb2  12712  limsuple  14138  limsupval2  14140  climsup  14329  ruclem11  14889  ruclem12  14890  prmreclem6  15544  imasaddfnlem  16104  imasvscafn  16113  cycsubgcl  17536  ghmrn  17589  ghmnsgima  17600  pgpssslw  17945  gexex  18172  dprdfcntz  18330  znf1o  19814  frlmlbs  20050  lindfrn  20074  ptcnplem  21329  kqt0lem  21444  isr0  21445  regr1lem2  21448  uzrest  21606  tmdgsum2  21805  imasf1oxmet  22085  imasf1omet  22086  bndth  22660  evth  22661  ovolficcss  23140  ovollb2lem  23158  ovolunlem1  23167  ovoliunlem1  23172  ovoliunlem2  23173  ovoliun2  23176  ovolscalem1  23183  ovolicc1  23186  voliunlem2  23221  voliunlem3  23222  ioombl1lem4  23231  uniioovol  23248  uniioombllem2  23252  uniioombllem3  23254  uniioombllem6  23257  volsup2  23274  vitalilem3  23280  mbfsup  23332  mbfinf  23333  mbflimsup  23334  itg1ge0  23354  itg1mulc  23372  itg1climres  23382  mbfi1fseqlem4  23386  itg2seq  23410  itg2monolem1  23418  itg2mono  23421  itg2i1fseq2  23424  itg2gt0  23428  itg2cnlem1  23429  itg2cn  23431  limciun  23559  plycpn  23943  hmopidmchi  28850  hmopidmpji  28851  rge0scvg  29769  mclsax  31166  mblfinlem2  33065  ismtyhmeolem  33221  nacsfix  36741  fnwe2lem2  37087  gneispace  37900  climinf  39229
  Copyright terms: Public domain W3C validator