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

Theorem rexrn 6850
 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 fvexd 6678 . 2 ((𝐹 Fn 𝐴𝑦𝐴) → (𝐹𝑦) ∈ V)
2 fvelrnb 6719 . . 3 (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦𝐴 (𝐹𝑦) = 𝑥))
3 eqcom 2765 . . . 4 ((𝐹𝑦) = 𝑥𝑥 = (𝐹𝑦))
43rexbii 3175 . . 3 (∃𝑦𝐴 (𝐹𝑦) = 𝑥 ↔ ∃𝑦𝐴 𝑥 = (𝐹𝑦))
52, 4bitrdi 290 . 2 (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦𝐴 𝑥 = (𝐹𝑦)))
6 rexrn.1 . . 3 (𝑥 = (𝐹𝑦) → (𝜑𝜓))
76adantl 485 . 2 ((𝐹 Fn 𝐴𝑥 = (𝐹𝑦)) → (𝜑𝜓))
81, 5, 7rexxfr2d 5284 1 (𝐹 Fn 𝐴 → (∃𝑥 ∈ ran 𝐹𝜑 ↔ ∃𝑦𝐴 𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∃wrex 3071  Vcvv 3409  ran crn 5529   Fn wfn 6335  ‘cfv 6340 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5173  ax-nul 5180  ax-pr 5302 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ral 3075  df-rex 3076  df-v 3411  df-sbc 3699  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5037  df-opab 5099  df-mpt 5117  df-id 5434  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-iota 6299  df-fun 6342  df-fn 6343  df-fv 6348 This theorem is referenced by:  elrnrexdm  6852  wemapwe  9206  rexanuz  14766  climsup  15087  supcvg  15272  ruclem12  15655  prmreclem6  16325  vdwmc  16382  znunit  20344  lmbr2  21972  lmff  22014  1stcfb  22158  imasf1oxms  23204  lebnumlem3  23677  lmmbr2  23972  lmcau  24026  bcthlem4  24040  mbfsup  24377  itg2monolem1  24463  itg2gt0  24473  ostth  26335  uhgrvtxedgiedgb  27041  dfnbgr3  27240  vdn0conngrumgrv2  28093  erdszelem10  32690  neibastop2lem  34132  filnetlem4  34153  mblfinlem2  35409  istotbnd3  35523  sstotbnd  35527  heibor  35573  nacsfix  40061  fnwe2lem2  40403  climinf  42649
 Copyright terms: Public domain W3C validator