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

Theorem rexbidva 3296
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
rexbidva.1 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
rexbidva (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rexbidva
StepHypRef Expression
1 rexbidva.1 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
21pm5.32da 579 . 2 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
32rexbidv2 3295 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wcel 2105  wrex 3139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-rex 3144
This theorem is referenced by:  rexbidv  3297  2rexbiia  3298  2rexbidva  3299  rexeqbidva  3427  frinxp  5628  onfr  6224  dfimafn  6722  funimass4  6724  fliftel  7051  fliftf  7057  isomin  7079  f1oiso  7093  releldm2  7733  oaass  8177  qsinxp  8363  qliftel  8370  fimaxg  8754  ordunifi  8757  supisolem  8926  fiming  8951  wemapwe  9149  cflim2  9674  cfsmolem  9681  alephsing  9687  brdom7disj  9942  brdom6disj  9943  alephreg  9993  nqereu  10340  1idpr  10440  map2psrpr  10521  axsup  10705  rereccl  11347  sup3  11587  infm3  11589  supadd  11598  creur  11621  creui  11622  nndiv  11672  nnrecl  11884  rpnnen1lem2  12366  rpnnen1lem1  12367  rpnnen1lem3  12368  rpnnen1lem5  12370  supxrbnd1  12704  supxrbnd2  12705  supxrbnd  12711  rabssnn0fi  13344  mptnn0fsupp  13355  expnlbnd  13584  wrdl3s3  14316  limsuplt  14826  clim2  14851  clim2c  14852  clim0c  14854  ello12  14863  elo12  14874  rlimresb  14912  climabs0  14932  sumeq2ii  15040  mertens  15232  prodeq2ii  15257  zprod  15281  nndivides  15607  alzdvds  15660  oddm1even  15682  oddnn02np1  15687  oddge22np1  15688  evennn02n  15689  evennn2n  15690  divalglem4  15737  divalgb  15745  modremain  15749  modprmn0modprm0  16134  vdwlem6  16312  vdwlem11  16317  vdw  16320  ramval  16334  imasleval  16804  dfiso3  17033  fullestrcsetc  17391  fullsetcestrc  17406  isipodrs  17761  ipodrsfi  17763  gsumpropd2lem  17879  mndpropd  17926  grppropd  18058  conjnmzb  18333  symgextfo  18481  symgfixfo  18498  sylow1lem2  18655  sylow3lem1  18683  sylow3lem3  18685  lsmelvalm  18707  lsmass  18726  iscyg3  18936  ghmcyg  18947  cycsubgcyg  18952  pgpfac1lem2  19128  pgpfac1lem4  19131  ablfac2  19142  dvdsr02  19337  crngunit  19343  dvdsrpropd  19377  lpigen  19959  znunit  20640  elfilspd  20877  scmatmats  21050  symgmatr01  21193  isclo  21625  iscnp3  21782  lmbrf  21798  cncnp  21818  lmss  21836  isnrm2  21896  cmpfi  21946  1stcfb  21983  1stccnp  22000  ptrescn  22177  txkgen  22190  xkoinjcn  22225  trfil3  22426  fmid  22498  lmflf  22543  txflf  22544  ptcmplem3  22592  tsmsf1o  22682  ucnprima  22820  metrest  23063  metcnp  23080  metcnp2  23081  txmetcnp  23086  metuel2  23104  metustbl  23105  psmetutop  23106  metucn  23110  evth2  23493  lmmbrf  23794  iscfil2  23798  fmcfil  23804  iscau2  23809  iscau4  23811  iscauf  23812  caucfil  23815  iscmet3lem3  23822  cfilresi  23827  causs  23830  lmclim  23835  ivth2  23985  ovolfioo  23997  ovolficc  23998  ovolshftlem1  24039  ovolscalem1  24043  volsup2  24135  ismbf3d  24184  mbfaddlem  24190  mbfsup  24194  mbfinf  24195  itg2seq  24272  itg2gt0  24290  ellimc2  24404  ellimc3  24406  rolle  24516  cmvth  24517  mvth  24518  dvlip  24519  dvivth  24536  lhop1lem  24539  deg1ldg  24615  ulm2  24902  ulmdvlem3  24919  dcubic  25351  mcubic  25352  cubic2  25353  rlimcnp  25471  ftalem3  25580  isppw2  25620  lgsquadlem2  25885  2lgslem1a  25895  dchrmusumlema  25997  dchrisum0lema  26018  tglowdim2l  26364  mirreu3  26368  oppcom  26458  iscgra1  26524  axsegcon  26641  axpasch  26655  axcontlem7  26684  usgr2pth0  27474  usgr2wspthon  27672  elwwlks2  27673  elwspths2spth  27674  rusgrnumwwlks  27681  clwwlkfo  27757  eclclwwlkn1  27782  eucrctshift  27950  fusgreg2wsp  28043  nmobndi  28480  nmounbi  28481  nmoo0  28496  h2hcau  28684  h2hlm  28685  shsel3  29020  pjhtheu2  29121  chscllem2  29343  adjbdln  29788  branmfn  29810  pjimai  29881  chrelati  30069  cdj3lem3  30143  cdj3lem3b  30145  dfimafnf  30310  ofpreima  30339  isarchi2  30742  submarchi  30743  archirng  30745  archiabl  30755  isarchiofld  30818  ellspds  30861  fedgmullem2  30926  ordtconnlem1  31067  lmdvg  31096  esumfsup  31229  dya2icoseg2  31436  eulerpartlemgh  31536  ballotlemodife  31655  ballotlemsima  31673  erdszelem10  32345  iscvm  32404  wsuclem  33010  etasslt  33172  seglelin  33475  outsideofeu  33490  opnrebl  33566  opnrebl2  33567  filnetlem4  33627  bj-finsumval0  34456  phpreu  34758  ptrest  34773  poimirlem3  34777  poimirlem4  34778  poimirlem17  34791  poimirlem26  34800  poimirlem27  34801  broucube  34808  mblfinlem1  34811  lmclim2  34916  caures  34918  isbnd3b  34946  heiborlem7  34978  heiborlem10  34981  rrncmslem  34993  isdrngo2  35119  erim2  35793  prter3  35900  islshpsm  35998  lsatfixedN  36027  lrelat  36032  eqlkr2  36118  lshpkrlem1  36128  lfl1dim  36139  eqlkr4  36183  ishlat3N  36372  hlsupr2  36405  hlrelat5N  36419  hlrelat  36420  cvrval5  36433  cvrat42  36462  athgt  36474  3dim0  36475  islln3  36528  llnexatN  36539  islpln3  36551  islvol3  36594  islvol5  36597  isline4N  36795  polval2N  36924  4atex3  37099  cdleme0ex2N  37242  cdlemefrs29cpre1  37416  cdlemb3  37624  cdlemg33c  37726  cdlemg33e  37728  dia1dim2  38080  cdlemm10N  38136  dib1dim2  38186  diclspsn  38212  dih1dimatlem  38347  dihatexv2  38357  djhcvat42  38433  dihjat1lem  38446  dvh4dimat  38456  dvh2dimatN  38458  lcfrlem9  38568  mapdval4N  38650  mapdcv  38678  elrfirn  39172  elrfirn2  39173  mrefg3  39185  diophin  39249  diophun  39250  diophren  39290  rmxycomplete  39394  wepwsolem  39522  fnwe2lem2  39531  islssfg  39550  ntrneineine0lem  40313  ntrneineine1lem  40314  ntrneiel2  40316  extoimad  40395  grumnudlem  40501  supsubc  41501  infxrbnd2  41517  supminfxr  41620  evthiccabs  41651  elicores  41689  clim2f  41797  clim2cf  41811  clim0cf  41815  clim2f2  41831  limsupub  41865  limsupmnflem  41881  limsupre2lem  41885  limsuplt2  41914  liminfreuzlem  41963  liminfltlem  41965  liminflimsupclim  41968  xlimmnfmpt  42004  xlimpnfmpt  42005  fourierdlem73  42345  fourierdlem83  42355  meaiuninc3v  42647  ovolval2  42807  dfaimafn  43245  iccelpart  43440  sprsymrelf  43504  sprsymrelfo  43506  fmtnoprmfac1  43574  fmtnoprmfac2  43576  fmtnofac2lem  43577  dfeven2  43661  dfodd3  43662  isomuspgrlem2d  43843  uspgrsprfo  43870  elbigo2  44510  rrxlinesc  44620  rrxlinec  44621  rrx2line  44625  rrx2vlinest  44626  itsclquadeu  44662
  Copyright terms: Public domain W3C validator