MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elrnmpt2 Structured version   Unicode version

Theorem elrnmpt2 6395
Description: Membership in the range of an operation class abstraction. (Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
Hypotheses
Ref Expression
rngop.1  |-  F  =  ( x  e.  A ,  y  e.  B  |->  C )
elrnmpt2.1  |-  C  e. 
_V
Assertion
Ref Expression
elrnmpt2  |-  ( D  e.  ran  F  <->  E. x  e.  A  E. y  e.  B  D  =  C )
Distinct variable groups:    y, A    x, y, D
Allowed substitution hints:    A( x)    B( x, y)    C( x, y)    F( x, y)

Proof of Theorem elrnmpt2
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 rngop.1 . . . 4  |-  F  =  ( x  e.  A ,  y  e.  B  |->  C )
21rnmpt2 6392 . . 3  |-  ran  F  =  { z  |  E. x  e.  A  E. y  e.  B  z  =  C }
32eleq2i 2480 . 2  |-  ( D  e.  ran  F  <->  D  e.  { z  |  E. x  e.  A  E. y  e.  B  z  =  C } )
4 elrnmpt2.1 . . . . . 6  |-  C  e. 
_V
5 eleq1 2474 . . . . . 6  |-  ( D  =  C  ->  ( D  e.  _V  <->  C  e.  _V ) )
64, 5mpbiri 233 . . . . 5  |-  ( D  =  C  ->  D  e.  _V )
76rexlimivw 2892 . . . 4  |-  ( E. y  e.  B  D  =  C  ->  D  e. 
_V )
87rexlimivw 2892 . . 3  |-  ( E. x  e.  A  E. y  e.  B  D  =  C  ->  D  e. 
_V )
9 eqeq1 2406 . . . 4  |-  ( z  =  D  ->  (
z  =  C  <->  D  =  C ) )
1092rexbidv 2924 . . 3  |-  ( z  =  D  ->  ( E. x  e.  A  E. y  e.  B  z  =  C  <->  E. x  e.  A  E. y  e.  B  D  =  C ) )
118, 10elab3 3202 . 2  |-  ( D  e.  { z  |  E. x  e.  A  E. y  e.  B  z  =  C }  <->  E. x  e.  A  E. y  e.  B  D  =  C )
123, 11bitri 249 1  |-  ( D  e.  ran  F  <->  E. x  e.  A  E. y  e.  B  D  =  C )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1405    e. wcel 1842   {cab 2387   E.wrex 2754   _Vcvv 3058   ran crn 4823    |-> cmpt2 6279
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-br 4395  df-opab 4453  df-cnv 4830  df-dm 4832  df-rn 4833  df-oprab 6281  df-mpt2 6282
This theorem is referenced by:  qexALT  11241  lsmelvalx  16982  efgtlen  17066  frgpnabllem1  17199  fmucndlem  21084  mbfimaopnlem  22352  tglnunirn  24316  tpr2rico  28333  mbfmco2  28699  br2base  28703  dya2icobrsiga  28710  dya2iocnrect  28715  dya2iocucvr  28718  sxbrsigalem2  28720  cntotbnd  31554  eldiophb  35031
  Copyright terms: Public domain W3C validator