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

Theorem rexbidva 3174
Description: Formula-building rule for restricted existential quantifier (deduction form). (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
ralbidva.1 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
rexbidva (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rexbidva
StepHypRef Expression
1 ralbidva.1 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
21pm5.32da 580 . 2 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
32rexbidv2 3172 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wcel 2107  wrex 3074
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3075
This theorem is referenced by:  rexbidv  3176  2rexbiia  3210  2rexbidva  3212  rexeqbidva  3325  frinxp  5719  onfr  6361  dfimafn  6910  funimass4  6912  fliftel  7259  fliftf  7265  isomin  7287  f1oiso  7301  releldm2  7980  oaass  8513  eldifsucnn  8615  cofonr  8625  naddunif  8644  qsinxp  8739  qliftel  8746  fimaxg  9241  ordunifi  9244  supisolem  9416  fiming  9441  wemapwe  9640  ttrcltr  9659  ttrclse  9670  frmin  9692  cflim2  10206  cfsmolem  10213  alephsing  10219  brdom7disj  10474  brdom6disj  10475  alephreg  10525  nqereu  10872  1idpr  10972  map2psrpr  11053  axsup  11237  rereccl  11880  sup3  12119  infm3  12121  supadd  12130  creur  12154  creui  12155  nndiv  12206  nnrecl  12418  rpnnen1lem2  12909  rpnnen1lem1  12910  rpnnen1lem3  12911  rpnnen1lem5  12913  supxrbnd1  13247  supxrbnd2  13248  supxrbnd  13254  rabssnn0fi  13898  mptnn0fsupp  13909  expnlbnd  14143  wrdl3s3  14858  limsuplt  15368  clim2  15393  clim2c  15394  clim0c  15396  ello12  15405  elo12  15416  rlimresb  15454  climabs0  15474  sumeq2ii  15585  mertens  15778  prodeq2ii  15803  zprod  15827  nndivides  16153  alzdvds  16209  oddm1even  16232  oddnn02np1  16237  oddge22np1  16238  evennn02n  16239  evennn2n  16240  divalglem4  16285  divalgb  16293  modremain  16297  modprmn0modprm0  16686  vdwlem6  16865  vdwlem11  16870  vdw  16873  ramval  16887  imasleval  17430  dfiso3  17663  fullestrcsetc  18046  fullsetcestrc  18061  isipodrs  18433  ipodrsfi  18435  gsumpropd2lem  18541  mndpropd  18588  grppropd  18772  conjnmzb  19050  symgextfo  19211  symgfixfo  19228  sylow1lem2  19388  sylow3lem1  19416  sylow3lem3  19418  lsmelvalm  19440  lsmass  19458  iscyg3  19670  ghmcyg  19680  cycsubgcyg  19685  pgpfac1lem2  19861  pgpfac1lem4  19864  ablfac2  19875  dvdsr02  20092  crngunit  20098  dvdsrpropd  20134  lpigen  20742  znunit  20986  elfilspd  21225  scmatmats  21876  symgmatr01  22019  isclo  22454  iscnp3  22611  lmbrf  22627  cncnp  22647  lmss  22665  isnrm2  22725  cmpfi  22775  1stcfb  22812  1stccnp  22829  ptrescn  23006  txkgen  23019  xkoinjcn  23054  trfil3  23255  fmid  23327  lmflf  23372  txflf  23373  ptcmplem3  23421  tsmsf1o  23512  ucnprima  23650  metrest  23896  metcnp  23913  metcnp2  23914  txmetcnp  23919  metuel2  23937  metustbl  23938  psmetutop  23939  metucn  23943  evth2  24339  lmmbrf  24642  iscfil2  24646  fmcfil  24652  iscau2  24657  iscau4  24659  iscauf  24660  caucfil  24663  iscmet3lem3  24670  cfilresi  24675  causs  24678  lmclim  24683  ivth2  24835  ovolfioo  24847  ovolficc  24848  ovolshftlem1  24889  ovolscalem1  24893  volsup2  24985  ismbf3d  25034  mbfaddlem  25040  mbfsup  25044  mbfinf  25045  itg2seq  25123  itg2gt0  25141  ellimc2  25257  ellimc3  25259  rolle  25370  cmvth  25371  mvth  25372  dvlip  25373  dvivth  25390  lhop1lem  25393  deg1ldg  25473  ulm2  25760  ulmdvlem3  25777  dcubic  26212  mcubic  26213  cubic2  26214  rlimcnp  26331  ftalem3  26440  isppw2  26480  lgsquadlem2  26745  2lgslem1a  26755  dchrmusumlema  26857  dchrisum0lema  26878  cofcutr  27265  lrrecfr  27277  addsrid  27298  addscom  27300  addsunif  27332  addsass  27335  negsunif  27372  mulsrid  27399  mulslid  27400  tglowdim2l  27634  mirreu3  27638  oppcom  27728  iscgra1  27794  axsegcon  27918  axpasch  27932  axcontlem7  27961  usgr2pth0  28755  usgr2wspthon  28952  elwwlks2  28953  elwspths2spth  28954  rusgrnumwwlks  28961  clwwlkfo  29036  eclclwwlkn1  29061  eucrctshift  29229  fusgreg2wsp  29322  nmobndi  29759  nmounbi  29760  nmoo0  29775  h2hcau  29963  h2hlm  29964  shsel3  30299  pjhtheu2  30400  chscllem2  30622  adjbdln  31067  branmfn  31089  pjimai  31160  chrelati  31348  cdj3lem3  31422  cdj3lem3b  31424  dfimafnf  31592  ofpreima  31623  isarchi2  32063  submarchi  32064  archirng  32066  archiabl  32076  isarchiofld  32152  ellspds  32197  lsmssass  32223  grplsm0l  32224  fedgmullem2  32365  elirng  32400  zarcls  32495  ordtconnlem1  32545  lmdvg  32574  esumfsup  32709  dya2icoseg2  32918  eulerpartlemgh  33018  ballotlemodife  33137  ballotlemsima  33155  nummin  33735  erdszelem10  33834  iscvm  33893  wsuclem  34439  seglelin  34730  outsideofeu  34745  opnrebl  34821  opnrebl2  34822  filnetlem4  34882  bj-finsumval0  35785  phpreu  36091  ptrest  36106  poimirlem3  36110  poimirlem4  36111  poimirlem17  36124  poimirlem26  36133  poimirlem27  36134  broucube  36141  mblfinlem1  36144  lmclim2  36246  caures  36248  isbnd3b  36273  heiborlem7  36305  heiborlem10  36308  rrncmslem  36320  isdrngo2  36446  erimeq2  37169  prter3  37373  islshpsm  37471  lsatfixedN  37500  lrelat  37505  eqlkr2  37591  lshpkrlem1  37601  lfl1dim  37612  eqlkr4  37656  ishlat3N  37845  hlsupr2  37879  hlrelat5N  37893  hlrelat  37894  cvrval5  37907  cvrat42  37936  athgt  37948  3dim0  37949  islln3  38002  llnexatN  38013  islpln3  38025  islvol3  38068  islvol5  38071  isline4N  38269  polval2N  38398  4atex3  38573  cdleme0ex2N  38716  cdlemefrs29cpre1  38890  cdlemb3  39098  cdlemg33c  39200  cdlemg33e  39202  dia1dim2  39554  cdlemm10N  39610  dib1dim2  39660  diclspsn  39686  dih1dimatlem  39821  dihatexv2  39831  djhcvat42  39907  dihjat1lem  39920  dvh4dimat  39930  dvh2dimatN  39932  lcfrlem9  40042  mapdval4N  40124  mapdcv  40152  infdesc  41010  elrfirn  41047  elrfirn2  41048  mrefg3  41060  diophin  41124  diophun  41125  diophren  41165  rmxycomplete  41270  wepwsolem  41398  fnwe2lem2  41407  islssfg  41426  unielss  41581  onmaxnelsup  41586  onsupnmax  41591  onsupeqnmax  41610  ntrneineine0lem  42429  ntrneineine1lem  42430  ntrneiel2  42432  extoimad  42511  grumnudlem  42639  supsubc  43661  infxrbnd2  43677  supminfxr  43773  evthiccabs  43808  elicores  43845  clim2f  43951  clim2cf  43965  clim0cf  43969  clim2f2  43985  limsupub  44019  limsupmnflem  44035  limsupre2lem  44039  limsuplt2  44068  liminfreuzlem  44117  liminfltlem  44119  liminflimsupclim  44122  xlimmnfmpt  44158  xlimpnfmpt  44159  fourierdlem73  44494  fourierdlem83  44504  meaiuninc3v  44799  ovolval2  44959  cfsetsnfsetfo  45368  dfaimafn  45471  iccelpart  45699  sprsymrelf  45761  sprsymrelfo  45763  fmtnoprmfac1  45831  fmtnoprmfac2  45833  fmtnofac2lem  45834  dfeven2  45915  dfodd3  45916  isomuspgrlem2d  46097  uspgrsprfo  46124  elbigo2  46712  rrxlinesc  46895  rrxlinec  46896  rrx2line  46900  rrx2vlinest  46901  itsclquadeu  46937
  Copyright terms: Public domain W3C validator