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

Theorem ovelrn 6708
 Description: A member of an operation's range is a value of the operation. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 30-Jan-2014.)
Assertion
Ref Expression
ovelrn (𝐹 Fn (𝐴 × 𝐵) → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥𝐴𝑦𝐵 𝐶 = (𝑥𝐹𝑦)))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦   𝑥,𝐹,𝑦

Proof of Theorem ovelrn
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 fnrnov 6705 . . 3 (𝐹 Fn (𝐴 × 𝐵) → ran 𝐹 = {𝑧 ∣ ∃𝑥𝐴𝑦𝐵 𝑧 = (𝑥𝐹𝑦)})
21eleq2d 2673 . 2 (𝐹 Fn (𝐴 × 𝐵) → (𝐶 ∈ ran 𝐹𝐶 ∈ {𝑧 ∣ ∃𝑥𝐴𝑦𝐵 𝑧 = (𝑥𝐹𝑦)}))
3 ovex 6577 . . . . . 6 (𝑥𝐹𝑦) ∈ V
4 eleq1 2676 . . . . . 6 (𝐶 = (𝑥𝐹𝑦) → (𝐶 ∈ V ↔ (𝑥𝐹𝑦) ∈ V))
53, 4mpbiri 247 . . . . 5 (𝐶 = (𝑥𝐹𝑦) → 𝐶 ∈ V)
65rexlimivw 3011 . . . 4 (∃𝑦𝐵 𝐶 = (𝑥𝐹𝑦) → 𝐶 ∈ V)
76rexlimivw 3011 . . 3 (∃𝑥𝐴𝑦𝐵 𝐶 = (𝑥𝐹𝑦) → 𝐶 ∈ V)
8 eqeq1 2614 . . . 4 (𝑧 = 𝐶 → (𝑧 = (𝑥𝐹𝑦) ↔ 𝐶 = (𝑥𝐹𝑦)))
982rexbidv 3039 . . 3 (𝑧 = 𝐶 → (∃𝑥𝐴𝑦𝐵 𝑧 = (𝑥𝐹𝑦) ↔ ∃𝑥𝐴𝑦𝐵 𝐶 = (𝑥𝐹𝑦)))
107, 9elab3 3327 . 2 (𝐶 ∈ {𝑧 ∣ ∃𝑥𝐴𝑦𝐵 𝑧 = (𝑥𝐹𝑦)} ↔ ∃𝑥𝐴𝑦𝐵 𝐶 = (𝑥𝐹𝑦))
112, 10syl6bb 275 1 (𝐹 Fn (𝐴 × 𝐵) → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥𝐴𝑦𝐵 𝐶 = (𝑥𝐹𝑦)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ∈ wcel 1977  {cab 2596  ∃wrex 2897  Vcvv 3173   × cxp 5036  ran crn 5039   Fn wfn 5799  (class class class)co 6549 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-csb 3500  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-iun 4457  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  df-ov 6552 This theorem is referenced by:  efgredlem  17983  efgcpbllemb  17991  gsumval3  18131  lecldbas  20833  blrnps  22023  blrn  22024  qdensere  22383  tgioo  22407  xrge0tsms  22445  ioorf  23147  ioorinv  23150  ioorcl  23151  dyaddisj  23170  dyadmax  23172  mbfid  23209  ismbfd  23213  hhssnv  27505  xrge0tsmsd  29116  iccllyscon  30486  rellyscon  30487  icoreelrnab  32378  relowlssretop  32387  relowlpssretop  32388  islptre  38686
 Copyright terms: Public domain W3C validator