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

Theorem rexbidva 3031
 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 671 . 2 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
32rexbidv2 3030 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∈ wcel 1977  ∃wrex 2897 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 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-rex 2902 This theorem is referenced by:  rexbidv  3034  2rexbiia  3037  2rexbidva  3038  rexeqbidva  3132  frinxp  5107  onfr  5680  dfimafn  6155  funimass4  6157  fliftel  6459  fliftf  6465  isomin  6487  f1oiso  6501  releldm2  7109  oaass  7528  qsinxp  7710  qliftel  7717  fimaxg  8092  ordunifi  8095  supisolem  8262  fiming  8287  wemapwe  8477  cflim2  8968  cfsmolem  8975  alephsing  8981  brdom7disj  9234  brdom6disj  9235  alephreg  9283  nqereu  9630  1idpr  9730  map2psrpr  9810  axsup  9992  rereccl  10622  sup3  10859  infm3  10861  supadd  10868  creur  10891  creui  10892  nndiv  10938  nnrecl  11167  rpnnen1lem2  11690  rpnnen1lem1  11691  rpnnen1lem3  11692  rpnnen1lem5  11694  rpnnen1lem1OLD  11697  rpnnen1lem3OLD  11698  rpnnen1lem5OLD  11700  supxrbnd1  12023  supxrbnd2  12024  supxrbnd  12030  rabssnn0fi  12647  mptnn0fsupp  12659  expnlbnd  12856  wrdl3s3  13553  limsuplt  14058  clim2  14083  clim2c  14084  clim0c  14086  ello12  14095  elo12  14106  rlimresb  14144  climabs0  14164  sumeq2ii  14271  mertens  14457  prodeq2ii  14482  zprod  14506  nndivides  14828  alzdvds  14880  oddm1even  14905  oddnn02np1  14910  oddge22np1  14911  evennn02n  14912  evennn2n  14913  divalglem4  14957  divalgb  14965  modremain  14970  modprmn0modprm0  15350  vdwlem6  15528  vdwlem11  15533  vdw  15536  ramval  15550  imasleval  16024  dfiso3  16256  fullestrcsetc  16614  fullsetcestrc  16629  isipodrs  16984  ipodrsfi  16986  gsumpropd2lem  17096  mndpropd  17139  grppropd  17260  conjnmzb  17518  symgextfo  17665  symgfixfo  17682  sylow1lem2  17837  sylow3lem1  17865  sylow3lem3  17867  lsmelvalm  17889  lsmass  17906  iscyg3  18111  ghmcyg  18120  cycsubgcyg  18125  pgpfac1lem2  18297  pgpfac1lem4  18300  ablfac2  18311  dvdsr02  18479  crngunit  18485  dvdsrpropd  18519  lpigen  19077  znunit  19731  elfilspd  19961  scmatmats  20136  symgmatr01  20279  isclo  20701  iscnp3  20858  lmbrf  20874  cncnp  20894  lmss  20912  isnrm2  20972  cmpfi  21021  1stcfb  21058  1stccnp  21075  ptrescn  21252  txkgen  21265  xkoinjcn  21300  trfil3  21502  fmid  21574  lmflf  21619  txflf  21620  ptcmplem3  21668  tsmsf1o  21758  ucnprima  21896  metrest  22139  metcnp  22156  metcnp2  22157  txmetcnp  22162  metuel2  22180  metustbl  22181  psmetutop  22182  metucn  22186  evth2  22567  lmmbrf  22868  iscfil2  22872  fmcfil  22878  iscau2  22883  iscau4  22885  iscauf  22886  caucfil  22889  iscmet3lem3  22896  cfilresi  22901  causs  22904  lmclim  22909  ivth2  23031  ovolfioo  23043  ovolficc  23044  ovolshftlem1  23084  ovolscalem1  23088  volsup2  23179  ismbf3d  23227  mbfaddlem  23233  mbfsup  23237  mbfinf  23238  itg2seq  23315  itg2gt0  23333  ellimc2  23447  ellimc3  23449  rolle  23557  cmvth  23558  mvth  23559  dvlip  23560  dvivth  23577  lhop1lem  23580  deg1ldg  23656  ulm2  23943  ulmdvlem3  23960  dcubic  24373  mcubic  24374  cubic2  24375  rlimcnp  24492  ftalem3  24601  isppw2  24641  lgsquadlem2  24906  2lgslem1a  24916  dchrmusumlema  24982  dchrisum0lema  25003  tglowdim2l  25345  mirreu3  25349  oppcom  25436  iscgra1  25502  axsegcon  25607  axpasch  25621  axcontlem7  25650  clwwlkfo  26325  eclclwwlkn1  26359  el2spthonot0  26398  usg2spthonot1  26417  rusgranumwlks  26483  usgreg2spot  26594  nmobndi  27014  nmounbi  27015  nmoo0  27030  h2hcau  27220  h2hlm  27221  shsel3  27558  pjhtheu2  27659  chscllem2  27881  adjbdln  28326  branmfn  28348  pjimai  28419  chrelati  28607  cdj3lem3  28681  cdj3lem3b  28683  dfimafnf  28817  ofpreima  28848  isarchi2  29070  submarchi  29071  archirng  29073  archiabl  29083  isarchiofld  29148  ordtconlem1  29298  lmdvg  29327  esumfsup  29459  dya2icoseg2  29667  eulerpartlemgh  29767  ballotlemodife  29886  ballotlemsima  29904  erdszelem10  30436  iscvm  30495  wsuclem  31017  wsuclemOLD  31018  seglelin  31393  outsideofeu  31408  opnrebl  31485  opnrebl2  31486  filnetlem4  31546  bj-finsumval0  32324  phpreu  32563  ptrest  32578  poimirlem3  32582  poimirlem4  32583  poimirlem17  32596  poimirlem26  32605  poimirlem27  32606  broucube  32613  mblfinlem1  32616  lmclim2  32724  caures  32726  isbnd3b  32754  heiborlem7  32786  heiborlem10  32789  rrncmslem  32801  isdrngo2  32927  prter3  33185  islshpsm  33285  lsatfixedN  33314  lrelat  33319  eqlkr2  33405  lshpkrlem1  33415  lfl1dim  33426  eqlkr4  33470  ishlat3N  33659  hlsupr2  33691  hlrelat5N  33705  hlrelat  33706  cvrval5  33719  cvrat42  33748  athgt  33760  3dim0  33761  islln3  33814  llnexatN  33825  islpln3  33837  islvol3  33880  islvol5  33883  isline4N  34081  polval2N  34210  4atex3  34385  cdleme0ex2N  34529  cdlemefrs29cpre1  34704  cdlemb3  34912  cdlemg33c  35014  cdlemg33e  35016  dia1dim2  35369  cdlemm10N  35425  dib1dim2  35475  diclspsn  35501  dih1dimatlem  35636  dihatexv2  35646  djhcvat42  35722  dihjat1lem  35735  dvh4dimat  35745  dvh2dimatN  35747  lcfrlem9  35857  mapdval4N  35939  mapdcv  35967  elrfirn  36276  elrfirn2  36277  mrefg3  36289  diophin  36354  diophun  36355  diophren  36395  rmxycomplete  36500  wepwsolem  36630  fnwe2lem2  36639  islssfg  36658  ntrneineine0lem  37401  ntrneineine1lem  37402  ntrneiel2  37404  extoimad  37486  supsubc  38510  infxrbnd2  38526  evthiccabs  38565  elicores  38607  clim2f  38703  clim2cf  38717  clim0cf  38721  clim2f2  38737  fourierdlem73  39072  fourierdlem83  39082  ovolval2  39534  dfaimafn  39894  iccelpart  39971  fmtnoprmfac1  40015  fmtnoprmfac2  40017  fmtnofac2lem  40018  dfeven2  40100  dfodd3  40101  usgr2pth0  40971  usgr2wspthon  41168  elwwlks2  41170  elwspths2spth  41171  rusgrnumwwlks  41177  clwwlksfo  41225  eclclwwlksn1  41259  eucrctshift  41411  fusgreg2wsp  41500  elbigo2  42144
 Copyright terms: Public domain W3C validator