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

Theorem rexbidva 3235
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 570 . 2 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
32rexbidv2 3234 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  wcel 2156  wrex 3095
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-rex 3100
This theorem is referenced by:  rexbidv  3238  2rexbiia  3241  2rexbidva  3242  rexeqbidva  3342  frinxp  5384  onfr  5974  dfimafn  6464  funimass4  6466  fliftel  6781  fliftf  6787  isomin  6809  f1oiso  6823  releldm2  7448  oaass  7876  qsinxp  8056  qliftel  8063  fimaxg  8444  ordunifi  8447  supisolem  8616  fiming  8641  wemapwe  8839  cflim2  9368  cfsmolem  9375  alephsing  9381  brdom7disj  9636  brdom6disj  9637  alephreg  9687  nqereu  10034  1idpr  10134  map2psrpr  10214  axsup  10396  rereccl  11026  sup3  11263  infm3  11265  supadd  11274  creur  11297  creui  11298  nndiv  11345  nnrecl  11555  rpnnen1lem2  12031  rpnnen1lem1  12032  rpnnen1lem3  12033  rpnnen1lem5  12035  supxrbnd1  12367  supxrbnd2  12368  supxrbnd  12374  rabssnn0fi  13007  mptnn0fsupp  13018  expnlbnd  13215  wrdl3s3  13928  limsuplt  14431  clim2  14456  clim2c  14457  clim0c  14459  ello12  14468  elo12  14479  rlimresb  14517  climabs0  14537  sumeq2ii  14644  mertens  14837  prodeq2ii  14862  zprod  14886  nndivides  15211  alzdvds  15263  oddm1even  15285  oddnn02np1  15290  oddge22np1  15291  evennn02n  15292  evennn2n  15293  divalglem4  15337  divalgb  15345  modremain  15349  modprmn0modprm0  15727  vdwlem6  15905  vdwlem11  15910  vdw  15913  ramval  15927  imasleval  16404  dfiso3  16635  fullestrcsetc  16994  fullsetcestrc  17009  isipodrs  17364  ipodrsfi  17366  gsumpropd2lem  17476  mndpropd  17519  grppropd  17640  conjnmzb  17895  symgextfo  18041  symgfixfo  18058  sylow1lem2  18213  sylow3lem1  18241  sylow3lem3  18243  lsmelvalm  18265  lsmass  18282  iscyg3  18487  ghmcyg  18496  cycsubgcyg  18501  pgpfac1lem2  18674  pgpfac1lem4  18677  ablfac2  18688  dvdsr02  18856  crngunit  18862  dvdsrpropd  18896  lpigen  19463  znunit  20117  elfilspd  20350  scmatmats  20526  symgmatr01  20670  isclo  21103  iscnp3  21260  lmbrf  21276  cncnp  21296  lmss  21314  isnrm2  21374  cmpfi  21423  1stcfb  21460  1stccnp  21477  ptrescn  21654  txkgen  21667  xkoinjcn  21702  trfil3  21903  fmid  21975  lmflf  22020  txflf  22021  ptcmplem3  22069  tsmsf1o  22159  ucnprima  22297  metrest  22540  metcnp  22557  metcnp2  22558  txmetcnp  22563  metuel2  22581  metustbl  22582  psmetutop  22583  metucn  22587  evth2  22970  lmmbrf  23270  iscfil2  23274  fmcfil  23280  iscau2  23285  iscau4  23287  iscauf  23288  caucfil  23291  iscmet3lem3  23298  cfilresi  23303  causs  23306  lmclim  23311  ivth2  23434  ovolfioo  23446  ovolficc  23447  ovolshftlem1  23488  ovolscalem1  23492  volsup2  23584  ismbf3d  23633  mbfaddlem  23639  mbfsup  23643  mbfinf  23644  itg2seq  23721  itg2gt0  23739  ellimc2  23853  ellimc3  23855  rolle  23965  cmvth  23966  mvth  23967  dvlip  23968  dvivth  23985  lhop1lem  23988  deg1ldg  24064  ulm2  24351  ulmdvlem3  24368  dcubic  24785  mcubic  24786  cubic2  24787  rlimcnp  24904  ftalem3  25013  isppw2  25053  lgsquadlem2  25318  2lgslem1a  25328  dchrmusumlema  25394  dchrisum0lema  25415  tglowdim2l  25757  mirreu3  25761  oppcom  25848  iscgra1  25914  axsegcon  26019  axpasch  26033  axcontlem7  26062  usgr2pth0  26887  usgr2wspthon  27105  elwwlks2  27106  elwspths2spth  27107  rusgrnumwwlks  27114  clwwlkfo  27197  eclclwwlkn1  27224  eucrctshift  27414  fusgreg2wsp  27509  nmobndi  27956  nmounbi  27957  nmoo0  27972  h2hcau  28162  h2hlm  28163  shsel3  28500  pjhtheu2  28601  chscllem2  28823  adjbdln  29268  branmfn  29290  pjimai  29361  chrelati  29549  cdj3lem3  29623  cdj3lem3b  29625  dfimafnf  29761  ofpreima  29790  isarchi2  30062  submarchi  30063  archirng  30065  archiabl  30075  isarchiofld  30140  ordtconnlem1  30293  lmdvg  30322  esumfsup  30455  dya2icoseg2  30663  eulerpartlemgh  30763  ballotlemodife  30882  ballotlemsima  30900  erdszelem10  31503  iscvm  31562  elintfv  31982  wsuclem  32089  etasslt  32239  seglelin  32542  outsideofeu  32557  opnrebl  32634  opnrebl2  32635  filnetlem4  32695  bj-finsumval0  33462  phpreu  33704  ptrest  33719  poimirlem3  33723  poimirlem4  33724  poimirlem17  33737  poimirlem26  33746  poimirlem27  33747  broucube  33754  mblfinlem1  33757  lmclim2  33863  caures  33865  isbnd3b  33893  heiborlem7  33925  heiborlem10  33928  rrncmslem  33940  isdrngo2  34066  prter3  34659  islshpsm  34758  lsatfixedN  34787  lrelat  34792  eqlkr2  34878  lshpkrlem1  34888  lfl1dim  34899  eqlkr4  34943  ishlat3N  35132  hlsupr2  35165  hlrelat5N  35179  hlrelat  35180  cvrval5  35193  cvrat42  35222  athgt  35234  3dim0  35235  islln3  35288  llnexatN  35299  islpln3  35311  islvol3  35354  islvol5  35357  isline4N  35555  polval2N  35684  4atex3  35859  cdleme0ex2N  36003  cdlemefrs29cpre1  36177  cdlemb3  36385  cdlemg33c  36487  cdlemg33e  36489  dia1dim2  36841  cdlemm10N  36897  dib1dim2  36947  diclspsn  36973  dih1dimatlem  37108  dihatexv2  37118  djhcvat42  37194  dihjat1lem  37207  dvh4dimat  37217  dvh2dimatN  37219  lcfrlem9  37329  mapdval4N  37411  mapdcv  37439  elrfirn  37758  elrfirn2  37759  mrefg3  37771  diophin  37836  diophun  37837  diophren  37877  rmxycomplete  37981  wepwsolem  38111  fnwe2lem2  38120  islssfg  38139  ntrneineine0lem  38879  ntrneineine1lem  38880  ntrneiel2  38882  extoimad  38962  supsubc  40047  infxrbnd2  40063  supminfxr  40171  evthiccabs  40200  elicores  40238  clim2f  40346  clim2cf  40360  clim0cf  40364  clim2f2  40380  limsupub  40414  limsupmnflem  40430  limsupre2lem  40434  limsuplt2  40463  liminfreuzlem  40512  liminfltlem  40514  liminflimsupclim  40517  xlimmnfmpt  40547  xlimpnfmpt  40548  fourierdlem73  40873  fourierdlem83  40883  meaiuninc3v  41178  ovolval2  41338  dfaimafn  41752  iccelpart  41942  fmtnoprmfac1  42050  fmtnoprmfac2  42052  fmtnofac2lem  42053  dfeven2  42135  dfodd3  42136  sprsymrelf  42311  sprsymrelfo  42313  uspgrsprfo  42322  elbigo2  42912
  Copyright terms: Public domain W3C validator