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

Theorem rexbidva 3078
Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 9-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 6-Dec-2019.) (Proof shortened by Wolf Lammen, 10-Dec-2019.)
Hypothesis
Ref Expression
rexbidva.1 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
rexbidva (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rexbidva
StepHypRef Expression
1 rexbidva.1 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
21pm5.32da 674 . 2 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
32rexbidv2 3077 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wcel 2030  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-rex 2947
This theorem is referenced by:  rexbidv  3081  2rexbiia  3084  2rexbidva  3085  rexeqbidva  3185  frinxp  5218  onfr  5801  dfimafn  6284  funimass4  6286  fliftel  6599  fliftf  6605  isomin  6627  f1oiso  6641  releldm2  7262  oaass  7686  qsinxp  7866  qliftel  7873  fimaxg  8248  ordunifi  8251  supisolem  8420  fiming  8445  wemapwe  8632  cflim2  9123  cfsmolem  9130  alephsing  9136  brdom7disj  9391  brdom6disj  9392  alephreg  9442  nqereu  9789  1idpr  9889  map2psrpr  9969  axsup  10151  rereccl  10781  sup3  11018  infm3  11020  supadd  11029  creur  11052  creui  11053  nndiv  11099  nnrecl  11328  rpnnen1lem2  11852  rpnnen1lem1  11853  rpnnen1lem3  11854  rpnnen1lem5  11856  rpnnen1lem1OLD  11859  rpnnen1lem3OLD  11860  rpnnen1lem5OLD  11862  supxrbnd1  12189  supxrbnd2  12190  supxrbnd  12196  rabssnn0fi  12825  mptnn0fsupp  12837  expnlbnd  13034  wrdl3s3  13751  limsuplt  14254  clim2  14279  clim2c  14280  clim0c  14282  ello12  14291  elo12  14302  rlimresb  14340  climabs0  14360  sumeq2ii  14467  mertens  14662  prodeq2ii  14687  zprod  14711  nndivides  15037  alzdvds  15089  oddm1even  15114  oddnn02np1  15119  oddge22np1  15120  evennn02n  15121  evennn2n  15122  divalglem4  15166  divalgb  15174  modremain  15179  modprmn0modprm0  15559  vdwlem6  15737  vdwlem11  15742  vdw  15745  ramval  15759  imasleval  16248  dfiso3  16480  fullestrcsetc  16838  fullsetcestrc  16853  isipodrs  17208  ipodrsfi  17210  gsumpropd2lem  17320  mndpropd  17363  grppropd  17484  conjnmzb  17742  symgextfo  17888  symgfixfo  17905  sylow1lem2  18060  sylow3lem1  18088  sylow3lem3  18090  lsmelvalm  18112  lsmass  18129  iscyg3  18334  ghmcyg  18343  cycsubgcyg  18348  pgpfac1lem2  18520  pgpfac1lem4  18523  ablfac2  18534  dvdsr02  18702  crngunit  18708  dvdsrpropd  18742  lpigen  19304  znunit  19960  elfilspd  20190  scmatmats  20365  symgmatr01  20508  isclo  20939  iscnp3  21096  lmbrf  21112  cncnp  21132  lmss  21150  isnrm2  21210  cmpfi  21259  1stcfb  21296  1stccnp  21313  ptrescn  21490  txkgen  21503  xkoinjcn  21538  trfil3  21739  fmid  21811  lmflf  21856  txflf  21857  ptcmplem3  21905  tsmsf1o  21995  ucnprima  22133  metrest  22376  metcnp  22393  metcnp2  22394  txmetcnp  22399  metuel2  22417  metustbl  22418  psmetutop  22419  metucn  22423  evth2  22806  lmmbrf  23106  iscfil2  23110  fmcfil  23116  iscau2  23121  iscau4  23123  iscauf  23124  caucfil  23127  iscmet3lem3  23134  cfilresi  23139  causs  23142  lmclim  23147  ivth2  23270  ovolfioo  23282  ovolficc  23283  ovolshftlem1  23323  ovolscalem1  23327  volsup2  23419  ismbf3d  23466  mbfaddlem  23472  mbfsup  23476  mbfinf  23477  itg2seq  23554  itg2gt0  23572  ellimc2  23686  ellimc3  23688  rolle  23798  cmvth  23799  mvth  23800  dvlip  23801  dvivth  23818  lhop1lem  23821  deg1ldg  23897  ulm2  24184  ulmdvlem3  24201  dcubic  24618  mcubic  24619  cubic2  24620  rlimcnp  24737  ftalem3  24846  isppw2  24886  lgsquadlem2  25151  2lgslem1a  25161  dchrmusumlema  25227  dchrisum0lema  25248  tglowdim2l  25590  mirreu3  25594  oppcom  25681  iscgra1  25747  axsegcon  25852  axpasch  25866  axcontlem7  25895  usgr2pth0  26717  usgr2wspthon  26932  elwwlks2  26933  elwspths2spth  26934  rusgrnumwwlks  26941  clwwlkfo  27013  eclclwwlkn1  27039  eucrctshift  27221  fusgreg2wsp  27316  nmobndi  27758  nmounbi  27759  nmoo0  27774  h2hcau  27964  h2hlm  27965  shsel3  28302  pjhtheu2  28403  chscllem2  28625  adjbdln  29070  branmfn  29092  pjimai  29163  chrelati  29351  cdj3lem3  29425  cdj3lem3b  29427  dfimafnf  29564  ofpreima  29593  isarchi2  29867  submarchi  29868  archirng  29870  archiabl  29880  isarchiofld  29945  ordtconnlem1  30098  lmdvg  30127  esumfsup  30260  dya2icoseg2  30468  eulerpartlemgh  30568  ballotlemodife  30687  ballotlemsima  30705  erdszelem10  31308  iscvm  31367  elintfv  31788  wsuclem  31895  etasslt  32045  seglelin  32348  outsideofeu  32363  opnrebl  32440  opnrebl2  32441  filnetlem4  32501  bj-finsumval0  33277  phpreu  33523  ptrest  33538  poimirlem3  33542  poimirlem4  33543  poimirlem17  33556  poimirlem26  33565  poimirlem27  33566  broucube  33573  mblfinlem1  33576  lmclim2  33684  caures  33686  isbnd3b  33714  heiborlem7  33746  heiborlem10  33749  rrncmslem  33761  isdrngo2  33887  prter3  34486  islshpsm  34585  lsatfixedN  34614  lrelat  34619  eqlkr2  34705  lshpkrlem1  34715  lfl1dim  34726  eqlkr4  34770  ishlat3N  34959  hlsupr2  34991  hlrelat5N  35005  hlrelat  35006  cvrval5  35019  cvrat42  35048  athgt  35060  3dim0  35061  islln3  35114  llnexatN  35125  islpln3  35137  islvol3  35180  islvol5  35183  isline4N  35381  polval2N  35510  4atex3  35685  cdleme0ex2N  35829  cdlemefrs29cpre1  36003  cdlemb3  36211  cdlemg33c  36313  cdlemg33e  36315  dia1dim2  36668  cdlemm10N  36724  dib1dim2  36774  diclspsn  36800  dih1dimatlem  36935  dihatexv2  36945  djhcvat42  37021  dihjat1lem  37034  dvh4dimat  37044  dvh2dimatN  37046  lcfrlem9  37156  mapdval4N  37238  mapdcv  37266  elrfirn  37575  elrfirn2  37576  mrefg3  37588  diophin  37653  diophun  37654  diophren  37694  rmxycomplete  37799  wepwsolem  37929  fnwe2lem2  37938  islssfg  37957  ntrneineine0lem  38698  ntrneineine1lem  38699  ntrneiel2  38701  extoimad  38781  supsubc  39882  infxrbnd2  39898  supminfxr  40007  evthiccabs  40036  elicores  40078  clim2f  40186  clim2cf  40200  clim0cf  40204  clim2f2  40220  limsupub  40254  limsupmnflem  40270  limsupre2lem  40274  limsuplt2  40303  liminfreuzlem  40352  liminfltlem  40354  liminflimsupclim  40357  xlimmnfmpt  40387  xlimpnfmpt  40388  fourierdlem73  40714  fourierdlem83  40724  meaiuninc3v  41019  ovolval2  41179  dfaimafn  41566  iccelpart  41694  fmtnoprmfac1  41802  fmtnoprmfac2  41804  fmtnofac2lem  41805  dfeven2  41887  dfodd3  41888  sprsymrelf  42070  sprsymrelfo  42072  uspgrsprfo  42081  elbigo2  42671
  Copyright terms: Public domain W3C validator