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

Theorem rexbidva 3030
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 670 . 2 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
32rexbidv2 3029 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  wcel 1976  wrex 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-rex 2901
This theorem is referenced by:  rexbidv  3033  2rexbiia  3036  2rexbidva  3037  rexeqbidva  3131  frinxp  5096  onfr  5665  dfimafn  6139  funimass4  6141  fliftel  6436  fliftf  6442  isomin  6464  f1oiso  6478  releldm2  7086  oaass  7505  qsinxp  7687  qliftel  7694  fimaxg  8069  ordunifi  8072  supisolem  8239  fiming  8264  wemapwe  8454  cflim2  8945  cfsmolem  8952  alephsing  8958  brdom7disj  9211  brdom6disj  9212  alephreg  9260  nqereu  9607  1idpr  9707  map2psrpr  9787  axsup  9964  rereccl  10594  sup3  10831  infm3  10833  supadd  10840  creur  10863  creui  10864  nndiv  10910  nnrecl  11139  rpnnen1lem2  11648  rpnnen1lem1  11649  rpnnen1lem3  11650  rpnnen1lem5  11652  rpnnen1lem1OLD  11655  rpnnen1lem3OLD  11656  rpnnen1lem5OLD  11658  supxrbnd1  11981  supxrbnd2  11982  supxrbnd  11988  rabssnn0fi  12604  mptnn0fsupp  12616  expnlbnd  12813  wrdl3s3  13501  limsuplt  14006  clim2  14031  clim2c  14032  clim0c  14034  ello12  14043  elo12  14054  rlimresb  14092  climabs0  14112  sumeq2ii  14219  mertens  14405  prodeq2ii  14430  zprod  14454  nndivides  14776  alzdvds  14828  oddm1even  14853  oddnn02np1  14858  oddge22np1  14859  evennn02n  14860  evennn2n  14861  divalglem4  14905  divalgb  14913  modremain  14918  modprmn0modprm0  15298  vdwlem6  15476  vdwlem11  15481  vdw  15484  ramval  15498  imasleval  15972  dfiso3  16204  fullestrcsetc  16562  fullsetcestrc  16577  isipodrs  16932  ipodrsfi  16934  gsumpropd2lem  17044  mndpropd  17087  grppropd  17208  conjnmzb  17466  symgextfo  17613  symgfixfo  17630  sylow1lem2  17785  sylow3lem1  17813  sylow3lem3  17815  lsmelvalm  17837  lsmass  17854  iscyg3  18059  ghmcyg  18068  cycsubgcyg  18073  pgpfac1lem2  18245  pgpfac1lem4  18248  ablfac2  18259  dvdsr02  18427  crngunit  18433  dvdsrpropd  18467  lpigen  19025  znunit  19678  elfilspd  19908  scmatmats  20083  symgmatr01  20226  isclo  20648  iscnp3  20805  lmbrf  20821  cncnp  20841  lmss  20859  isnrm2  20919  cmpfi  20968  1stcfb  21005  1stccnp  21022  ptrescn  21199  txkgen  21212  xkoinjcn  21247  trfil3  21449  fmid  21521  lmflf  21566  txflf  21567  ptcmplem3  21615  tsmsf1o  21705  ucnprima  21843  metrest  22086  metcnp  22103  metcnp2  22104  txmetcnp  22109  metuel2  22127  metustbl  22128  psmetutop  22129  metucn  22133  evth2  22514  lmmbrf  22812  iscfil2  22816  fmcfil  22822  iscau2  22827  iscau4  22829  iscauf  22830  caucfil  22833  iscmet3lem3  22840  cfilresi  22845  causs  22848  lmclim  22853  ivth2  22975  ovolfioo  22987  ovolficc  22988  ovolshftlem1  23028  ovolscalem1  23032  volsup2  23123  ismbf3d  23171  mbfaddlem  23177  mbfsup  23181  mbfinf  23182  itg2seq  23259  itg2gt0  23277  ellimc2  23391  ellimc3  23393  rolle  23501  cmvth  23502  mvth  23503  dvlip  23504  dvivth  23521  lhop1lem  23524  deg1ldg  23600  ulm2  23887  ulmdvlem3  23904  dcubic  24317  mcubic  24318  cubic2  24319  rlimcnp  24436  ftalem3  24545  isppw2  24585  lgsquadlem2  24850  2lgslem1a  24860  dchrmusumlema  24926  dchrisum0lema  24947  tglowdim2l  25290  mirreu3  25294  oppcom  25381  iscgra1  25447  axsegcon  25552  axpasch  25566  axcontlem7  25595  clwwlkfo  26118  eclclwwlkn1  26152  el2spthonot0  26191  usg2spthonot1  26210  rusgranumwlks  26276  usgreg2spot  26387  nmobndi  26807  nmounbi  26808  nmoo0  26823  h2hcau  27013  h2hlm  27014  shsel3  27351  pjhtheu2  27452  chscllem2  27674  adjbdln  28119  branmfn  28141  pjimai  28212  chrelati  28400  cdj3lem3  28474  cdj3lem3b  28476  dfimafnf  28610  ofpreima  28641  isarchi2  28863  submarchi  28864  archirng  28866  archiabl  28876  isarchiofld  28941  ordtconlem1  29091  lmdvg  29120  esumfsup  29252  dya2icoseg2  29460  eulerpartlemgh  29560  ballotlemodife  29679  ballotlemsima  29697  erdszelem10  30229  iscvm  30288  wsuclem  30810  wsuclemOLD  30811  seglelin  31186  outsideofeu  31201  opnrebl  31278  opnrebl2  31279  filnetlem4  31339  bj-finsumval0  32107  phpreu  32346  ptrest  32361  poimirlem3  32365  poimirlem4  32366  poimirlem17  32379  poimirlem26  32388  poimirlem27  32389  broucube  32396  mblfinlem1  32399  lmclim2  32507  caures  32509  isbnd3b  32537  heiborlem7  32569  heiborlem10  32572  rrncmslem  32584  isdrngo2  32710  prter3  32968  islshpsm  33068  lsatfixedN  33097  lrelat  33102  eqlkr2  33188  lshpkrlem1  33198  lfl1dim  33209  eqlkr4  33253  ishlat3N  33442  hlsupr2  33474  hlrelat5N  33488  hlrelat  33489  cvrval5  33502  cvrat42  33531  athgt  33543  3dim0  33544  islln3  33597  llnexatN  33608  islpln3  33620  islvol3  33663  islvol5  33666  isline4N  33864  polval2N  33993  4atex3  34168  cdleme0ex2N  34312  cdlemefrs29cpre1  34487  cdlemb3  34695  cdlemg33c  34797  cdlemg33e  34799  dia1dim2  35152  cdlemm10N  35208  dib1dim2  35258  diclspsn  35284  dih1dimatlem  35419  dihatexv2  35429  djhcvat42  35505  dihjat1lem  35518  dvh4dimat  35528  dvh2dimatN  35530  lcfrlem9  35640  mapdval4N  35722  mapdcv  35750  elrfirn  36059  elrfirn2  36060  mrefg3  36072  diophin  36137  diophun  36138  diophren  36178  rmxycomplete  36283  wepwsolem  36413  fnwe2lem2  36422  islssfg  36441  ntrneineine0lem  37184  ntrneineine1lem  37185  ntrneiel2  37187  extoimad  37269  supsubc  38293  infxrbnd2  38309  evthiccabs  38348  elicores  38390  clim2f  38486  clim2cf  38500  clim0cf  38504  clim2f2  38520  fourierdlem73  38855  fourierdlem83  38865  ovolval2  39317  dfaimafn  39678  iccelpart  39755  fmtnoprmfac1  39799  fmtnoprmfac2  39801  fmtnofac2lem  39802  dfeven2  39884  dfodd3  39885  usgr2pth0  40952  usgr2wspthon  41149  elwwlks2  41151  elwspths2spth  41152  rusgrnumwwlks  41158  clwwlksfo  41206  eclclwwlksn1  41240  eucrctshift  41392  fusgreg2wsp  41481  elbigo2  42125
  Copyright terms: Public domain W3C validator