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

Theorem rexbidva 3293
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 3292 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wcel 2105  wrex 3136
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 3141
This theorem is referenced by:  rexbidv  3294  2rexbiia  3295  2rexbidva  3296  rexeqbidva  3424  frinxp  5627  onfr  6223  dfimafn  6721  funimass4  6723  fliftel  7051  fliftf  7057  isomin  7079  f1oiso  7093  releldm2  7731  oaass  8176  qsinxp  8362  qliftel  8369  fimaxg  8753  ordunifi  8756  supisolem  8925  fiming  8950  wemapwe  9148  cflim2  9673  cfsmolem  9680  alephsing  9686  brdom7disj  9941  brdom6disj  9942  alephreg  9992  nqereu  10339  1idpr  10439  map2psrpr  10520  axsup  10704  rereccl  11346  sup3  11586  infm3  11588  supadd  11597  creur  11620  creui  11621  nndiv  11671  nnrecl  11883  rpnnen1lem2  12364  rpnnen1lem1  12365  rpnnen1lem3  12366  rpnnen1lem5  12368  supxrbnd1  12702  supxrbnd2  12703  supxrbnd  12709  rabssnn0fi  13342  mptnn0fsupp  13353  expnlbnd  13582  wrdl3s3  14314  limsuplt  14824  clim2  14849  clim2c  14850  clim0c  14852  ello12  14861  elo12  14872  rlimresb  14910  climabs0  14930  sumeq2ii  15038  mertens  15230  prodeq2ii  15255  zprod  15279  nndivides  15605  alzdvds  15658  oddm1even  15680  oddnn02np1  15685  oddge22np1  15686  evennn02n  15687  evennn2n  15688  divalglem4  15735  divalgb  15743  modremain  15747  modprmn0modprm0  16132  vdwlem6  16310  vdwlem11  16315  vdw  16318  ramval  16332  imasleval  16802  dfiso3  17031  fullestrcsetc  17389  fullsetcestrc  17404  isipodrs  17759  ipodrsfi  17761  gsumpropd2lem  17877  mndpropd  17924  grppropd  18056  conjnmzb  18331  symgextfo  18479  symgfixfo  18496  sylow1lem2  18653  sylow3lem1  18681  sylow3lem3  18683  lsmelvalm  18705  lsmass  18724  iscyg3  18934  ghmcyg  18945  cycsubgcyg  18950  pgpfac1lem2  19126  pgpfac1lem4  19129  ablfac2  19140  dvdsr02  19335  crngunit  19341  dvdsrpropd  19375  lpigen  19957  znunit  20638  elfilspd  20875  scmatmats  21048  symgmatr01  21191  isclo  21623  iscnp3  21780  lmbrf  21796  cncnp  21816  lmss  21834  isnrm2  21894  cmpfi  21944  1stcfb  21981  1stccnp  21998  ptrescn  22175  txkgen  22188  xkoinjcn  22223  trfil3  22424  fmid  22496  lmflf  22541  txflf  22542  ptcmplem3  22590  tsmsf1o  22680  ucnprima  22818  metrest  23061  metcnp  23078  metcnp2  23079  txmetcnp  23084  metuel2  23102  metustbl  23103  psmetutop  23104  metucn  23108  evth2  23491  lmmbrf  23792  iscfil2  23796  fmcfil  23802  iscau2  23807  iscau4  23809  iscauf  23810  caucfil  23813  iscmet3lem3  23820  cfilresi  23825  causs  23828  lmclim  23833  ivth2  23983  ovolfioo  23995  ovolficc  23996  ovolshftlem1  24037  ovolscalem1  24041  volsup2  24133  ismbf3d  24182  mbfaddlem  24188  mbfsup  24192  mbfinf  24193  itg2seq  24270  itg2gt0  24288  ellimc2  24402  ellimc3  24404  rolle  24514  cmvth  24515  mvth  24516  dvlip  24517  dvivth  24534  lhop1lem  24537  deg1ldg  24613  ulm2  24900  ulmdvlem3  24917  dcubic  25351  mcubic  25352  cubic2  25353  rlimcnp  25470  ftalem3  25579  isppw2  25619  lgsquadlem2  25884  2lgslem1a  25894  dchrmusumlema  25996  dchrisum0lema  26017  tglowdim2l  26363  mirreu3  26367  oppcom  26457  iscgra1  26523  axsegcon  26640  axpasch  26654  axcontlem7  26683  usgr2pth0  27473  usgr2wspthon  27671  elwwlks2  27672  elwspths2spth  27673  rusgrnumwwlks  27680  clwwlkfo  27756  eclclwwlkn1  27781  eucrctshift  27949  fusgreg2wsp  28042  nmobndi  28479  nmounbi  28480  nmoo0  28495  h2hcau  28683  h2hlm  28684  shsel3  29019  pjhtheu2  29120  chscllem2  29342  adjbdln  29787  branmfn  29809  pjimai  29880  chrelati  30068  cdj3lem3  30142  cdj3lem3b  30144  dfimafnf  30309  ofpreima  30338  isarchi2  30741  submarchi  30742  archirng  30744  archiabl  30754  isarchiofld  30817  ellspds  30860  fedgmullem2  30925  ordtconnlem1  31066  lmdvg  31095  esumfsup  31228  dya2icoseg2  31435  eulerpartlemgh  31535  ballotlemodife  31654  ballotlemsima  31672  erdszelem10  32344  iscvm  32403  wsuclem  33009  etasslt  33171  seglelin  33474  outsideofeu  33489  opnrebl  33565  opnrebl2  33566  filnetlem4  33626  bj-finsumval0  34455  phpreu  34757  ptrest  34772  poimirlem3  34776  poimirlem4  34777  poimirlem17  34790  poimirlem26  34799  poimirlem27  34800  broucube  34807  mblfinlem1  34810  lmclim2  34914  caures  34916  isbnd3b  34944  heiborlem7  34976  heiborlem10  34979  rrncmslem  34991  isdrngo2  35117  erim2  35791  prter3  35898  islshpsm  35996  lsatfixedN  36025  lrelat  36030  eqlkr2  36116  lshpkrlem1  36126  lfl1dim  36137  eqlkr4  36181  ishlat3N  36370  hlsupr2  36403  hlrelat5N  36417  hlrelat  36418  cvrval5  36431  cvrat42  36460  athgt  36472  3dim0  36473  islln3  36526  llnexatN  36537  islpln3  36549  islvol3  36592  islvol5  36595  isline4N  36793  polval2N  36922  4atex3  37097  cdleme0ex2N  37240  cdlemefrs29cpre1  37414  cdlemb3  37622  cdlemg33c  37724  cdlemg33e  37726  dia1dim2  38078  cdlemm10N  38134  dib1dim2  38184  diclspsn  38210  dih1dimatlem  38345  dihatexv2  38355  djhcvat42  38431  dihjat1lem  38444  dvh4dimat  38454  dvh2dimatN  38456  lcfrlem9  38566  mapdval4N  38648  mapdcv  38676  elrfirn  39170  elrfirn2  39171  mrefg3  39183  diophin  39247  diophun  39248  diophren  39288  rmxycomplete  39392  wepwsolem  39520  fnwe2lem2  39529  islssfg  39548  ntrneineine0lem  40311  ntrneineine1lem  40312  ntrneiel2  40314  extoimad  40393  grumnudlem  40498  supsubc  41497  infxrbnd2  41513  supminfxr  41616  evthiccabs  41647  elicores  41685  clim2f  41793  clim2cf  41807  clim0cf  41811  clim2f2  41827  limsupub  41861  limsupmnflem  41877  limsupre2lem  41881  limsuplt2  41910  liminfreuzlem  41959  liminfltlem  41961  liminflimsupclim  41964  xlimmnfmpt  42000  xlimpnfmpt  42001  fourierdlem73  42341  fourierdlem83  42351  meaiuninc3v  42643  ovolval2  42803  dfaimafn  43241  iccelpart  43470  sprsymrelf  43534  sprsymrelfo  43536  fmtnoprmfac1  43604  fmtnoprmfac2  43606  fmtnofac2lem  43607  dfeven2  43691  dfodd3  43692  isomuspgrlem2d  43873  uspgrsprfo  43900  elbigo2  44540  rrxlinesc  44650  rrxlinec  44651  rrx2line  44655  rrx2vlinest  44656  itsclquadeu  44692
  Copyright terms: Public domain W3C validator