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

Theorem rexbidva 3255
 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 582 . 2 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
32rexbidv2 3254 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∈ wcel 2111  ∃wrex 3107 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-rex 3112 This theorem is referenced by:  rexbidv  3256  2rexbiia  3257  2rexbidva  3258  rexeqbidva  3371  frinxp  5599  onfr  6199  dfimafn  6704  funimass4  6706  fliftel  7042  fliftf  7048  isomin  7070  f1oiso  7084  releldm2  7727  oaass  8173  qsinxp  8359  qliftel  8366  fimaxg  8752  ordunifi  8755  supisolem  8924  fiming  8949  wemapwe  9147  cflim2  9677  cfsmolem  9684  alephsing  9690  brdom7disj  9945  brdom6disj  9946  alephreg  9996  nqereu  10343  1idpr  10443  map2psrpr  10524  axsup  10708  rereccl  11350  sup3  11588  infm3  11590  supadd  11599  creur  11622  creui  11623  nndiv  11674  nnrecl  11886  rpnnen1lem2  12367  rpnnen1lem1  12368  rpnnen1lem3  12369  rpnnen1lem5  12371  supxrbnd1  12705  supxrbnd2  12706  supxrbnd  12712  rabssnn0fi  13352  mptnn0fsupp  13363  expnlbnd  13593  wrdl3s3  14320  limsuplt  14831  clim2  14856  clim2c  14857  clim0c  14859  ello12  14868  elo12  14879  rlimresb  14917  climabs0  14937  sumeq2ii  15045  mertens  15237  prodeq2ii  15262  zprod  15286  nndivides  15612  alzdvds  15665  oddm1even  15687  oddnn02np1  15692  oddge22np1  15693  evennn02n  15694  evennn2n  15695  divalglem4  15740  divalgb  15748  modremain  15752  modprmn0modprm0  16137  vdwlem6  16315  vdwlem11  16320  vdw  16323  ramval  16337  imasleval  16809  dfiso3  17038  fullestrcsetc  17396  fullsetcestrc  17411  isipodrs  17766  ipodrsfi  17768  gsumpropd2lem  17884  mndpropd  17931  grppropd  18114  conjnmzb  18389  symgextfo  18546  symgfixfo  18563  sylow1lem2  18720  sylow3lem1  18748  sylow3lem3  18750  lsmelvalm  18772  lsmass  18791  iscyg3  19002  ghmcyg  19013  cycsubgcyg  19018  pgpfac1lem2  19194  pgpfac1lem4  19197  ablfac2  19208  dvdsr02  19406  crngunit  19412  dvdsrpropd  19446  lpigen  20026  znunit  20260  elfilspd  20497  scmatmats  21126  symgmatr01  21269  isclo  21702  iscnp3  21859  lmbrf  21875  cncnp  21895  lmss  21913  isnrm2  21973  cmpfi  22023  1stcfb  22060  1stccnp  22077  ptrescn  22254  txkgen  22267  xkoinjcn  22302  trfil3  22503  fmid  22575  lmflf  22620  txflf  22621  ptcmplem3  22669  tsmsf1o  22760  ucnprima  22898  metrest  23141  metcnp  23158  metcnp2  23159  txmetcnp  23164  metuel2  23182  metustbl  23183  psmetutop  23184  metucn  23188  evth2  23575  lmmbrf  23876  iscfil2  23880  fmcfil  23886  iscau2  23891  iscau4  23893  iscauf  23894  caucfil  23897  iscmet3lem3  23904  cfilresi  23909  causs  23912  lmclim  23917  ivth2  24069  ovolfioo  24081  ovolficc  24082  ovolshftlem1  24123  ovolscalem1  24127  volsup2  24219  ismbf3d  24268  mbfaddlem  24274  mbfsup  24278  mbfinf  24279  itg2seq  24356  itg2gt0  24374  ellimc2  24490  ellimc3  24492  rolle  24603  cmvth  24604  mvth  24605  dvlip  24606  dvivth  24623  lhop1lem  24626  deg1ldg  24703  ulm2  24990  ulmdvlem3  25007  dcubic  25442  mcubic  25443  cubic2  25444  rlimcnp  25561  ftalem3  25670  isppw2  25710  lgsquadlem2  25975  2lgslem1a  25985  dchrmusumlema  26087  dchrisum0lema  26108  tglowdim2l  26454  mirreu3  26458  oppcom  26548  iscgra1  26614  axsegcon  26731  axpasch  26745  axcontlem7  26774  usgr2pth0  27564  usgr2wspthon  27761  elwwlks2  27762  elwspths2spth  27763  rusgrnumwwlks  27770  clwwlkfo  27845  eclclwwlkn1  27870  eucrctshift  28038  fusgreg2wsp  28131  nmobndi  28568  nmounbi  28569  nmoo0  28584  h2hcau  28772  h2hlm  28773  shsel3  29108  pjhtheu2  29209  chscllem2  29431  adjbdln  29876  branmfn  29898  pjimai  29969  chrelati  30157  cdj3lem3  30231  cdj3lem3b  30233  dfimafnf  30405  ofpreima  30438  isarchi2  30874  submarchi  30875  archirng  30877  archiabl  30887  isarchiofld  30951  ellspds  30994  lsmssass  31019  fedgmullem2  31129  zarcls  31242  ordtconnlem1  31292  lmdvg  31321  esumfsup  31454  dya2icoseg2  31661  eulerpartlemgh  31761  ballotlemodife  31880  ballotlemsima  31898  nummin  32489  erdszelem10  32575  iscvm  32634  wsuclem  33240  etasslt  33402  seglelin  33705  outsideofeu  33720  opnrebl  33796  opnrebl2  33797  filnetlem4  33857  bj-finsumval0  34719  phpreu  35060  ptrest  35075  poimirlem3  35079  poimirlem4  35080  poimirlem17  35093  poimirlem26  35102  poimirlem27  35103  broucube  35110  mblfinlem1  35113  lmclim2  35215  caures  35217  isbnd3b  35242  heiborlem7  35274  heiborlem10  35277  rrncmslem  35289  isdrngo2  35415  erim2  36090  prter3  36197  islshpsm  36295  lsatfixedN  36324  lrelat  36329  eqlkr2  36415  lshpkrlem1  36425  lfl1dim  36436  eqlkr4  36480  ishlat3N  36669  hlsupr2  36702  hlrelat5N  36716  hlrelat  36717  cvrval5  36730  cvrat42  36759  athgt  36771  3dim0  36772  islln3  36825  llnexatN  36836  islpln3  36848  islvol3  36891  islvol5  36894  isline4N  37092  polval2N  37221  4atex3  37396  cdleme0ex2N  37539  cdlemefrs29cpre1  37713  cdlemb3  37921  cdlemg33c  38023  cdlemg33e  38025  dia1dim2  38377  cdlemm10N  38433  dib1dim2  38483  diclspsn  38509  dih1dimatlem  38644  dihatexv2  38654  djhcvat42  38730  dihjat1lem  38743  dvh4dimat  38753  dvh2dimatN  38755  lcfrlem9  38865  mapdval4N  38947  mapdcv  38975  elrfirn  39679  elrfirn2  39680  mrefg3  39692  diophin  39756  diophun  39757  diophren  39797  rmxycomplete  39901  wepwsolem  40029  fnwe2lem2  40038  islssfg  40057  ntrneineine0lem  40829  ntrneineine1lem  40830  ntrneiel2  40832  extoimad  40911  grumnudlem  41036  supsubc  42028  infxrbnd2  42044  supminfxr  42146  evthiccabs  42176  elicores  42213  clim2f  42321  clim2cf  42335  clim0cf  42339  clim2f2  42355  limsupub  42389  limsupmnflem  42405  limsupre2lem  42409  limsuplt2  42438  liminfreuzlem  42487  liminfltlem  42489  liminflimsupclim  42492  xlimmnfmpt  42528  xlimpnfmpt  42529  fourierdlem73  42864  fourierdlem83  42874  meaiuninc3v  43166  ovolval2  43326  dfaimafn  43764  iccelpart  43993  sprsymrelf  44055  sprsymrelfo  44057  fmtnoprmfac1  44125  fmtnoprmfac2  44127  fmtnofac2lem  44128  dfeven2  44210  dfodd3  44211  isomuspgrlem2d  44392  uspgrsprfo  44419  elbigo2  45007  rrxlinesc  45190  rrxlinec  45191  rrx2line  45195  rrx2vlinest  45196  itsclquadeu  45232
 Copyright terms: Public domain W3C validator