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

Theorem ralbidva 2900
Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 4-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 29-Dec-2019.)
Hypothesis
Ref Expression
ralbidva.1  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
Assertion
Ref Expression
ralbidva  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)

Proof of Theorem ralbidva
StepHypRef Expression
1 ralbidva.1 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
21pm5.74da 687 . 2  |-  ( ph  ->  ( ( x  e.  A  ->  ps )  <->  ( x  e.  A  ->  ch ) ) )
32ralbidv2 2899 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    e. wcel 1767   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2819
This theorem is referenced by:  ralbidv  2903  2ralbidva  2906  raleqbidva  3074  ordunisssuc  4980  poinxp  5063  soinxp  5064  frinxp  5065  fnmptfvd  5984  funimass3  5997  fnnfpeq0  6092  fnsuppresOLD  6121  cocan1  6182  cocan2  6183  isores2  6217  isoini2  6223  ofrfval  6532  ofrfval2  6541  tfindsg2  6680  f1oweALT  6768  fnsuppres  6927  dfsmo2  7018  smores  7023  smores2  7025  ac6sfi  7764  fimaxg  7767  ordunifi  7770  isfinite2  7778  fipreima  7826  supisolem  7931  ordiso2  7940  ordtypelem7  7949  cantnf  8112  cantnfOLD  8134  wemapwe  8139  wemapweOLD  8140  rankval3b  8244  rankonidlem  8246  iscard  8356  acndom  8432  dfac12lem3  8525  kmlem2  8531  cflim2  8643  cfsmolem  8650  ttukeylem6  8894  alephreg  8957  suplem2pr  9431  axsup  9660  sup3  10500  infm3  10502  suprleub  10507  dfinfmr  10520  infmrgelb  10523  ofsubeq0  10533  ofsubge0  10535  zextlt  10935  prime  10941  suprfinzcl  10975  indstr  11150  supxr2  11505  supxrbnd1  11513  supxrbnd2  11514  supxrleub  11518  supxrbnd  11520  infmxrgelb  11526  fzshftral  11765  mptnn0fsupp  12071  swrdeq  12634  swrdsymbeq  12635  clim  13280  rlim  13281  clim2  13290  clim2c  13291  clim0c  13293  ello1mpt  13307  lo1o1  13318  o1lo1  13323  climabs0  13371  o1compt  13373  rlimdiv  13431  geomulcvg  13648  mertenslem2  13657  mertens  13658  rpnnen2  13820  sqrt2irr  13843  pc11  14262  pcz  14263  1arith  14304  vdwlem8  14365  vdwlem11  14368  vdw  14371  ramval  14385  pwsle  14747  mrieqvd  14893  mreacs  14913  cidpropd  14966  ismon2  14990  monpropd  14993  isepi  14996  isepi2  14997  subsubc  15080  funcres2b  15124  funcpropd  15127  isfull2  15138  isfth2  15142  fucsect  15199  fucinv  15200  pospropd  15621  ipodrsfi  15650  tsrss  15710  mndpropd  15764  grpidpropd  15765  grppropd  15878  issubg4  16025  gass  16144  gsmsymgrfixlem1  16257  gsmsymgreqlem2  16261  gexdvds  16410  gexdvds2  16411  subgpgp  16423  sylow3lem6  16458  efgval2  16548  efgsp1  16561  dprdf11  16865  dprdf11OLD  16872  subgdmdprd  16883  rngpropd  17031  abvpropd  17291  lsspropd  17463  lbspropd  17545  assapropd  17775  psrbaglefi  17822  psrbaglefiOLD  17823  psrbagconf1o  17825  gsumbagdiaglem  17826  mplmonmul  17925  gsumply1eq  18146  phlpropd  18485  ishil2  18545  lindfmm  18657  islindf4  18668  islindf5  18669  scmatf1  18828  cpmatmcllem  19014  cpmatmcl  19015  decpmataa0  19064  decpmatmulsumfsupp  19069  pmatcollpw2lem  19073  pm2mpmhmlem1  19114  tgss2  19283  isclo  19382  neips  19408  opnnei  19415  isperf3  19448  ssidcn  19550  lmbrf  19555  cnnei  19577  cnrest2  19581  lmss  19593  lmres  19595  ist1-2  19642  ist1-3  19644  isreg2  19672  cmpfi  19702  bwth  19704  1stccn  19758  subislly  19776  kgencn  19820  ptclsg  19879  ptcnplem  19885  xkococnlem  19923  xkoinjcn  19951  tgqtop  19976  qtopcn  19978  fbflim  20240  flimrest  20247  flfnei  20255  isflf  20257  cnflf  20266  fclsopn  20278  fclsbas  20285  fclsrest  20288  isfcf  20298  cnfcf  20306  ptcmplem3  20317  tmdgsum2  20358  eltsms  20394  tsmsgsum  20400  tsmsgsumOLD  20403  tsmssubm  20407  tsmsf1o  20410  utopsnneiplem  20513  ismet2  20599  prdsxmetlem  20634  elmopn2  20711  prdsbl  20757  metss  20774  metrest  20790  metcnp  20807  metcnp2  20808  metcn  20809  metucnOLD  20854  metucn  20855  nrginvrcn  20963  metdsge  21116  divcn  21135  elcncf2  21157  mulc1cncf  21172  cncfmet  21175  evth2  21223  lmmbr2  21461  lmmbrf  21464  iscfil2  21468  cfil3i  21471  iscau2  21479  iscau4  21481  iscauf  21482  caucfil  21485  iscmet3lem3  21492  cfilres  21498  causs  21500  lmclim  21504  rrxmet  21598  evthicc2  21635  cniccbdd  21636  ovolfioo  21642  ovolficc  21643  ismbl2  21701  mbfsup  21834  mbfinf  21835  mbflimsup  21836  0plef  21842  mbfi1flim  21893  xrge0f  21901  itg2mulclem  21916  itgeqa  21983  ellimc2  22044  ellimc3  22046  limcflf  22048  cnlimc  22055  dvferm1  22149  dvferm2  22151  rolle  22154  dvivthlem1  22172  ftc1lem6  22205  itgsubst  22213  mdegle0  22240  deg1leb  22258  plydivex  22455  ulm2  22542  ulmcaulem  22551  ulmcau  22552  ulmdvlem3  22559  abelthlem9  22597  abelth  22598  rlimcnp  23051  ftalem3  23104  issqf  23166  sqf11  23169  dvdsmulf1o  23226  dchrelbas4  23274  dchrinv  23292  2sqlem6  23400  chpo1ubb  23422  dchrmusumlema  23434  dchrisum0lema  23455  ostth3  23579  eqeelen  23911  brbtwn2  23912  colinearalg  23917  axcgrid  23923  axsegconlem1  23924  ax5seglem4  23939  ax5seglem5  23940  axbtwnid  23946  axpasch  23948  axeuclidlem  23969  axcontlem2  23972  axcontlem4  23974  axcontlem7  23977  axcontlem12  23982  wwlknext  24428  clwwlkel  24497  clwwlkf  24498  wwlkext2clwwlk  24507  wwlksubclwwlk  24508  clwlkfclwwlk  24548  extwwlkfablem2  24783  numclwwlkovf2ex  24791  isgrpo2  24903  nmounbi  25395  blocnilem  25423  isph  25441  phoeqi  25477  h2hcau  25600  h2hlm  25601  hial2eq2  25728  hoeq1  26453  hoeq2  26454  adjsym  26456  cnvadj  26515  hhcno  26527  hhcnf  26528  adjvalval  26560  leop2  26747  leoptri  26759  mdbr2  26919  dmdbr2  26926  mddmd2  26932  cdj3lem3b  27063  fcnvgreu  27214  toslublem  27345  tosglblem  27347  submarchi  27420  isarchi3  27421  lmdvg  27599  eulerpartlemd  27973  subfacp1lem3  28294  subfacp1lem5  28296  dfrdg2  28833  itg2gt0cn  29675  ftc1cnnc  29694  opnrebl  29743  lmclim2  29882  caures  29884  sstotbnd2  29901  rrnmet  29956  rrncmslem  29959  isdrngo3  29993  isidlc  30043  wepwsolem  30619  fnwe2lem2  30629  islnm2  30656  isprm7  30823  caofcan  30856  evthiccabs  31121  ellimcabssub0  31187  climf  31192  idlimc  31196  clim2f  31206  clim2cf  31220  clim0cf  31224  fourierdlem70  31505  fourierdlem71  31506  fourierdlem73  31508  fourierdlem80  31515  fourierdlem83  31518  fourierdlem87  31522  sgrpplusgaop  31962  islinindfis  32149  cvrval2  34089  isat3  34122  iscvlat2N  34139  glbconN  34191  ltrneq  34963  cdlemefrs29clN  35213  cdlemefrs32fva  35214  cdleme32fva  35251  cdlemk33N  35723  cdlemk34  35724  cdlemkid3N  35747  cdlemkid4  35748  diaglbN  35870  dibglbN  35981  dihglbcpreN  36115  dihglblem6  36155  hdmap1eulem  36639  hdmap1eulemOLDN  36640  hdmapoc  36749  hlhilocv  36775
  Copyright terms: Public domain W3C validator