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

Theorem rexrn 6269
 Description: Restricted existential 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
rexrn (𝐹 Fn 𝐴 → (∃𝑥 ∈ ran 𝐹𝜑 ↔ ∃𝑦𝐴 𝜓))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐹,𝑦   𝜓,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem rexrn
StepHypRef Expression
1 fvex 6113 . . 3 (𝐹𝑦) ∈ V
21a1i 11 . 2 ((𝐹 Fn 𝐴𝑦𝐴) → (𝐹𝑦) ∈ V)
3 fvelrnb 6153 . . 3 (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦𝐴 (𝐹𝑦) = 𝑥))
4 eqcom 2617 . . . 4 ((𝐹𝑦) = 𝑥𝑥 = (𝐹𝑦))
54rexbii 3023 . . 3 (∃𝑦𝐴 (𝐹𝑦) = 𝑥 ↔ ∃𝑦𝐴 𝑥 = (𝐹𝑦))
63, 5syl6bb 275 . 2 (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦𝐴 𝑥 = (𝐹𝑦)))
7 rexrn.1 . . 3 (𝑥 = (𝐹𝑦) → (𝜑𝜓))
87adantl 481 . 2 ((𝐹 Fn 𝐴𝑥 = (𝐹𝑦)) → (𝜑𝜓))
92, 6, 8rexxfr2d 4809 1 (𝐹 Fn 𝐴 → (∃𝑥 ∈ ran 𝐹𝜑 ↔ ∃𝑦𝐴 𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∃wrex 2897  Vcvv 3173  ran crn 5039   Fn wfn 5799  ‘cfv 5804 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-iota 5768  df-fun 5806  df-fn 5807  df-fv 5812 This theorem is referenced by:  elrnrexdm  6271  wemapwe  8477  rexanuz  13933  climsup  14248  supcvg  14427  ruclem12  14809  prmreclem6  15463  vdwmc  15520  znunit  19731  lmbr2  20873  lmff  20915  1stcfb  21058  imasf1oxms  22104  lebnumlem3  22570  lmmbr2  22865  lmcau  22919  bcthlem4  22932  mbfsup  23237  itg2monolem1  23323  itg2gt0  23333  ostth  25128  uhgrvtxedgiedgb  25810  erdszelem10  30436  neibastop2lem  31525  filnetlem4  31546  mblfinlem2  32617  istotbnd3  32740  sstotbnd  32744  heibor  32790  nacsfix  36293  fnwe2lem2  36639  climinf  38673  dfnbgr3  40562  vdn0conngrumgrv2  41363
 Copyright terms: Public domain W3C validator