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

Theorem rexbidva 2965
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:   ,

Proof of Theorem rexbidva
StepHypRef Expression
1 rexbidva.1 . . 3
21pm5.32da 641 . 2
32rexbidv2 2964 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  e.wcel 1818  E.wrex 2808
This theorem is referenced by:  rexbidv  2968  2rexbiia  2973  2rexbidva  2974  rexeqbidva  3071  onfr  4922  frinxp  5070  dfimafn  5922  funimass4  5924  fconstfvOLD  6134  fliftel  6207  fliftf  6213  isomin  6233  f1oiso  6247  releldm2  6850  oaass  7229  qsinxp  7406  qliftel  7413  fimaxg  7787  ordunifi  7790  supisolem  7952  wemapwe  8160  wemapweOLD  8161  cflim2  8664  cfsmolem  8671  alephsing  8677  brdom7disj  8930  brdom6disj  8931  alephreg  8978  nqereu  9328  1idpr  9428  map2psrpr  9508  axsup  9681  rereccl  10287  sup3  10525  infm3  10527  creur  10555  creui  10556  nndiv  10601  nnrecl  10818  rpnnen1lem1  11237  rpnnen1lem2  11238  rpnnen1lem3  11239  rpnnen1lem5  11241  supxrbnd1  11542  supxrbnd2  11543  supxrbnd  11549  rabssnn0fi  12095  mptnn0fsupp  12103  expnlbnd  12296  limsuplt  13302  clim2  13327  clim2c  13328  clim0c  13330  ello12  13339  elo12  13350  rlimresb  13388  climabs0  13408  sumeq2ii  13515  mertens  13695  prodeq2ii  13720  zprod  13744  alzdvds  14036  oddm1even  14047  divalglem4  14054  divalgb  14062  modprmn0modprm0  14332  vdwlem6  14504  vdwlem11  14509  vdw  14512  ramval  14526  imasleval  14938  isipodrs  15791  ipodrsfi  15793  gsumpropd2lem  15900  mndpropd  15946  grppropd  16068  conjnmzb  16301  symgextfo  16447  symgfixfo  16464  sylow1lem2  16619  sylow3lem1  16647  sylow3lem3  16649  lsmelvalm  16671  lsmass  16688  iscyg3  16889  ghmcyg  16898  cycsubgcyg  16903  pgpfac1lem2  17126  pgpfac1lem4  17129  ablfac2  17140  dvdsr02  17305  crngunit  17311  dvdsrpropd  17345  lpigen  17904  znunit  18602  elfilspd  18838  scmatmats  19013  symgmatr01  19156  isclo  19588  iscnp3  19745  lmbrf  19761  cncnp  19781  lmss  19799  isnrm2  19859  cmpfi  19908  bwthOLD  19911  1stcfb  19946  1stccnp  19963  ptrescn  20140  txkgen  20153  xkoinjcn  20188  trfil3  20389  fmid  20461  lmflf  20506  txflf  20507  ptcmplem3  20554  tsmsf1o  20647  ucnprima  20785  metrest  21027  metcnp  21044  metcnp2  21045  txmetcnp  21050  metuel2  21082  metustblOLD  21083  metustbl  21084  metutopOLD  21085  psmetutop  21086  metucnOLD  21091  metucn  21092  evth2  21460  lmmbrf  21701  iscfil2  21705  fmcfil  21711  iscau2  21716  iscau4  21718  iscauf  21719  caucfil  21722  iscmet3lem3  21729  cfilresi  21734  causs  21737  lmclim  21741  ivth2  21867  ovolfioo  21879  ovolficc  21880  ovolshftlem1  21920  ovolscalem1  21924  volsup2  22014  ismbf3d  22061  mbfaddlem  22067  mbfsup  22071  mbfinf  22072  itg2seq  22149  itg2gt0  22167  ellimc2  22281  ellimc3  22283  rolle  22391  cmvth  22392  mvth  22393  dvlip  22394  dvivth  22411  lhop1lem  22414  deg1ldg  22492  ulm2  22780  ulmdvlem3  22797  dcubic  23177  mcubic  23178  cubic2  23179  rlimcnp  23295  ftalem3  23348  isppw2  23389  lgsquadlem2  23630  dchrmusumlema  23678  dchrisum0lema  23699  tglowdim2l  24031  mirreu3  24035  oppcom  24116  axsegcon  24230  axpasch  24244  axcontlem7  24273  clwwlkfo  24797  eclclwwlkn1  24832  el2spthonot0  24871  usg2spthonot1  24890  rusgranumwlks  24956  usgreg2spot  25067  nmobndi  25690  nmounbi  25691  nmoo0  25706  h2hcau  25896  h2hlm  25897  shsel3  26233  pjhtheu2  26334  chscllem2  26556  adjbdln  27002  branmfn  27024  pjimai  27095  chrelati  27283  cdj3lem3  27357  cdj3lem3b  27359  dfimafnf  27473  ofpreima  27507  isarchi2  27729  submarchi  27730  archirng  27732  archiabl  27742  isarchiofld  27807  ordtconlem1  27906  lmdvg  27935  esumfsup  28076  dya2icoseg2  28249  eulerpartlemgh  28317  ballotlemodife  28436  ballotlemsima  28454  erdszelem10  28644  iscvm  28704  wsuclem  29381  seglelin  29766  outsideofeu  29781  supadd  30042  ptrest  30048  mblfinlem1  30051  opnrebl  30138  opnrebl2  30139  filnetlem4  30199  lmclim2  30251  caures  30253  isbnd3b  30281  heiborlem7  30313  heiborlem10  30316  rrncmslem  30328  isdrngo2  30361  prter3  30623  elrfirn  30627  elrfirn2  30628  mrefg3  30640  diophin  30706  diophun  30707  diophren  30747  rmxycomplete  30853  wepwsolem  30987  fnwe2lem2  30997  islssfg  31016  evthiccabs  31529  clim2f  31642  clim2cf  31656  clim0cf  31660  fourierdlem73  31962  fourierdlem83  31972  dfaimafn  32250  usgra2pth0  32355  dfiso3  32569  fullestrcsetc  32657  fullsetcestrc  32672  bj-finsumval0  34663  islshpsm  34705  lsatfixedN  34734  lrelat  34739  eqlkr2  34825  lshpkrlem1  34835  lfl1dim  34846  eqlkr4  34890  ishlat3N  35079  hlsupr2  35111  hlrelat5N  35125  hlrelat  35126  cvrval5  35139  cvrat42  35168  athgt  35180  3dim0  35181  islln3  35234  llnexatN  35245  islpln3  35257  islvol3  35300  islvol5  35303  isline4N  35501  polval2N  35630  4atex3  35805  cdleme0ex2N  35949  cdlemefrs29cpre1  36124  cdlemb3  36332  cdlemg33c  36434  cdlemg33e  36436  dia1dim2  36789  cdlemm10N  36845  dib1dim2  36895  diclspsn  36921  dih1dimatlem  37056  dihatexv2  37066  djhcvat42  37142  dihjat1lem  37155  dvh4dimat  37165  dvh2dimatN  37167  lcfrlem9  37277  mapdval4N  37359  mapdcv  37387  extoimad  37981
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-rex 2813
  Copyright terms: Public domain W3C validator