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

Theorem rexrnmpt 5960
Description: A restricted quantifier over an image set. (Contributed by Mario Carneiro, 20-Aug-2015.)
Hypotheses
Ref Expression
ralrnmpt.1  |-  F  =  ( x  e.  A  |->  B )
ralrnmpt.2  |-  ( y  =  B  ->  ( ps 
<->  ch ) )
Assertion
Ref Expression
rexrnmpt  |-  ( A. x  e.  A  B  e.  V  ->  ( E. y  e.  ran  F ps 
<->  E. x  e.  A  ch ) )
Distinct variable groups:    x, A    y, B    ch, y    y, F    ps, x
Allowed substitution hints:    ps( y)    ch( x)    A( y)    B( x)    F( x)    V( x, y)

Proof of Theorem rexrnmpt
StepHypRef Expression
1 ralrnmpt.1 . . . 4  |-  F  =  ( x  e.  A  |->  B )
2 ralrnmpt.2 . . . . 5  |-  ( y  =  B  ->  ( ps 
<->  ch ) )
32notbid 292 . . . 4  |-  ( y  =  B  ->  ( -.  ps  <->  -.  ch )
)
41, 3ralrnmpt 5959 . . 3  |-  ( A. x  e.  A  B  e.  V  ->  ( A. y  e.  ran  F  -.  ps 
<-> 
A. x  e.  A  -.  ch ) )
54notbid 292 . 2  |-  ( A. x  e.  A  B  e.  V  ->  ( -. 
A. y  e.  ran  F  -.  ps  <->  -.  A. x  e.  A  -.  ch )
)
6 dfrex2 2847 . 2  |-  ( E. y  e.  ran  F ps 
<->  -.  A. y  e. 
ran  F  -.  ps )
7 dfrex2 2847 . 2  |-  ( E. x  e.  A  ch  <->  -. 
A. x  e.  A  -.  ch )
85, 6, 73bitr4g 288 1  |-  ( A. x  e.  A  B  e.  V  ->  ( E. y  e.  ran  F ps 
<->  E. x  e.  A  ch ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    = wceq 1399    e. wcel 1836   A.wral 2746   E.wrex 2747    |-> cmpt 4442   ran crn 4931
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374  ax-sep 4505  ax-nul 4513  ax-pow 4560  ax-pr 4618
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2236  df-mo 2237  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-ne 2593  df-ral 2751  df-rex 2752  df-rab 2755  df-v 3053  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3729  df-if 3875  df-sn 3962  df-pr 3964  df-op 3968  df-uni 4181  df-br 4385  df-opab 4443  df-mpt 4444  df-id 4726  df-xp 4936  df-rel 4937  df-cnv 4938  df-co 4939  df-dm 4940  df-rn 4941  df-res 4942  df-ima 4943  df-iota 5477  df-fun 5515  df-fn 5516  df-fv 5521
This theorem is referenced by:  onoviun  6954  onnseq  6955  ghmcyg  17038  pgpfac1lem2  17262  pgpfac1lem3  17264  pgpfac1lem4  17265  pptbas  19617  lly1stc  20105  txbas  20176  eltsms  20739  tsmsf1o  20755  metutopOLD  21193  psmetutop  21194  xrge0tsms  21447  fmcfil  21819  ellimc2  22389  limcflf  22393  xrge0tsmsd  27964  cntotbnd  30498
  Copyright terms: Public domain W3C validator