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

Theorem ralbidva 2879
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 2878 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 1804   A.wral 2793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691
This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2798
This theorem is referenced by:  ralbidv  2882  2ralbidva  2885  raleqbidva  3056  ordunisssuc  4970  poinxp  5053  soinxp  5054  frinxp  5055  fnmptfvd  5975  funimass3  5988  fnnfpeq0  6087  fnsuppresOLD  6116  cocan1  6179  cocan2  6180  isores2  6214  isoini2  6220  ofrfval  6533  ofrfval2  6542  tfindsg2  6681  f1oweALT  6769  fnsuppres  6929  dfsmo2  7020  smores  7025  smores2  7027  ac6sfi  7766  fimaxg  7769  ordunifi  7772  isfinite2  7780  fipreima  7828  supisolem  7934  ordiso2  7943  ordtypelem7  7952  cantnf  8115  cantnfOLD  8137  wemapwe  8142  wemapweOLD  8143  rankval3b  8247  rankonidlem  8249  iscard  8359  acndom  8435  dfac12lem3  8528  kmlem2  8534  cflim2  8646  cfsmolem  8653  ttukeylem6  8897  alephreg  8960  suplem2pr  9434  axsup  9663  sup3  10507  infm3  10509  suprleub  10514  dfinfmr  10527  infmrgelb  10530  ofsubeq0  10540  ofsubge0  10542  zextlt  10944  prime  10950  suprfinzcl  10984  indstr  11160  supxr2  11515  supxrbnd1  11523  supxrbnd2  11524  supxrleub  11528  supxrbnd  11530  infmxrgelb  11536  fzshftral  11776  mptnn0fsupp  12084  swrdeq  12652  swrdsymbeq  12653  clim  13298  rlim  13299  clim2  13308  clim2c  13309  clim0c  13311  ello1mpt  13325  lo1o1  13336  o1lo1  13341  climabs0  13389  o1compt  13391  rlimdiv  13449  geomulcvg  13666  mertenslem2  13675  mertens  13676  rpnnen2  13940  sqrt2irr  13963  pc11  14384  pcz  14385  1arith  14426  vdwlem8  14487  vdwlem11  14490  vdw  14493  ramval  14507  pwsle  14870  mrieqvd  15016  mreacs  15036  cidpropd  15086  ismon2  15110  monpropd  15113  isepi  15116  isepi2  15117  subsubc  15200  funcres2b  15244  funcpropd  15247  isfull2  15258  isfth2  15262  fucsect  15319  fucinv  15320  pospropd  15742  ipodrsfi  15771  tsrss  15831  grpidpropd  15866  mndpropd  15924  grppropd  16046  issubg4  16198  gass  16317  gsmsymgrfixlem1  16430  gsmsymgreqlem2  16434  gexdvds  16582  gexdvds2  16583  subgpgp  16595  sylow3lem6  16630  efgval2  16720  efgsp1  16733  dprdf11  17041  dprdf11OLD  17048  subgdmdprd  17059  ringpropd  17208  abvpropd  17469  lsspropd  17641  lbspropd  17723  assapropd  17954  psrbaglefi  18001  psrbaglefiOLD  18002  psrbagconf1o  18004  gsumbagdiaglem  18005  mplmonmul  18104  gsumply1eq  18325  phlpropd  18667  ishil2  18727  lindfmm  18839  islindf4  18850  islindf5  18851  scmatf1  19010  cpmatmcllem  19196  cpmatmcl  19197  decpmataa0  19246  decpmatmulsumfsupp  19251  pmatcollpw2lem  19255  pm2mpmhmlem1  19296  tgss2  19466  isclo  19565  neips  19591  opnnei  19598  isperf3  19631  ssidcn  19733  lmbrf  19738  cnnei  19760  cnrest2  19764  lmss  19776  lmres  19778  ist1-2  19825  ist1-3  19827  isreg2  19855  cmpfi  19885  bwth  19887  1stccn  19941  subislly  19959  kgencn  20034  ptclsg  20093  ptcnplem  20099  xkococnlem  20137  xkoinjcn  20165  tgqtop  20190  qtopcn  20192  fbflim  20454  flimrest  20461  flfnei  20469  isflf  20471  cnflf  20480  fclsopn  20492  fclsbas  20499  fclsrest  20502  isfcf  20512  cnfcf  20520  ptcmplem3  20531  tmdgsum2  20572  eltsms  20608  tsmsgsum  20614  tsmsgsumOLD  20617  tsmssubm  20621  tsmsf1o  20624  utopsnneiplem  20727  ismet2  20813  prdsxmetlem  20848  elmopn2  20925  prdsbl  20971  metss  20988  metrest  21004  metcnp  21021  metcnp2  21022  metcn  21023  metucnOLD  21068  metucn  21069  nrginvrcn  21177  metdsge  21330  divcn  21349  elcncf2  21371  mulc1cncf  21386  cncfmet  21389  evth2  21437  lmmbr2  21675  lmmbrf  21678  iscfil2  21682  cfil3i  21685  iscau2  21693  iscau4  21695  iscauf  21696  caucfil  21699  iscmet3lem3  21706  cfilres  21712  causs  21714  lmclim  21718  rrxmet  21812  evthicc2  21849  cniccbdd  21850  ovolfioo  21856  ovolficc  21857  ismbl2  21915  mbfsup  22048  mbfinf  22049  mbflimsup  22050  0plef  22056  mbfi1flim  22107  xrge0f  22115  itg2mulclem  22130  itgeqa  22197  ellimc2  22258  ellimc3  22260  limcflf  22262  cnlimc  22269  dvferm1  22363  dvferm2  22365  rolle  22368  dvivthlem1  22386  ftc1lem6  22419  itgsubst  22427  mdegle0  22454  deg1leb  22472  plydivex  22669  ulm2  22756  ulmcaulem  22765  ulmcau  22766  ulmdvlem3  22773  abelthlem9  22811  abelth  22812  rlimcnp  23271  ftalem3  23324  issqf  23386  sqf11  23389  dvdsmulf1o  23446  dchrelbas4  23494  dchrinv  23512  2sqlem6  23620  chpo1ubb  23642  dchrmusumlema  23654  dchrisum0lema  23675  ostth3  23799  eqeelen  24183  brbtwn2  24184  colinearalg  24189  axcgrid  24195  axsegconlem1  24196  ax5seglem4  24211  ax5seglem5  24212  axbtwnid  24218  axpasch  24220  axeuclidlem  24241  axcontlem2  24244  axcontlem4  24246  axcontlem7  24249  axcontlem12  24254  wwlknext  24700  clwwlkel  24769  clwwlkf  24770  wwlkext2clwwlk  24779  wwlksubclwwlk  24780  clwlkfclwwlk  24820  extwwlkfablem2  25054  numclwwlkovf2ex  25062  isgrpo2  25175  nmounbi  25667  blocnilem  25695  isph  25713  phoeqi  25749  h2hcau  25872  h2hlm  25873  hial2eq2  26000  hoeq1  26725  hoeq2  26726  adjsym  26728  cnvadj  26787  hhcno  26799  hhcnf  26800  adjvalval  26832  leop2  27019  leoptri  27031  mdbr2  27191  dmdbr2  27198  mddmd2  27204  cdj3lem3b  27335  toslublem  27632  tosglblem  27634  submarchi  27707  isarchi3  27708  cmpcref  27830  lmdvg  27912  eulerpartlemd  28282  subfacp1lem3  28603  subfacp1lem5  28605  dfrdg2  29203  itg2gt0cn  30045  ftc1cnnc  30064  opnrebl  30113  lmclim2  30226  caures  30228  sstotbnd2  30245  rrnmet  30300  rrncmslem  30303  isdrngo3  30337  isidlc  30387  wepwsolem  30962  fnwe2lem2  30972  islnm2  30999  isprm7  31168  caofcan  31204  evthiccabs  31465  ellimcabssub0  31531  climf  31536  clim2f  31550  clim2cf  31564  clim0cf  31568  fourierdlem70  31848  fourierdlem71  31849  fourierdlem73  31851  fourierdlem80  31858  fourierdlem83  31861  fourierdlem87  31865  islinindfis  32785  cvrval2  34739  isat3  34772  iscvlat2N  34789  glbconN  34841  ltrneq  35613  cdlemefrs29clN  35865  cdlemefrs32fva  35866  cdleme32fva  35903  cdlemk33N  36375  cdlemk34  36376  cdlemkid3N  36399  cdlemkid4  36400  diaglbN  36522  dibglbN  36633  dihglbcpreN  36767  dihglblem6  36807  hdmap1eulem  37291  hdmap1eulemOLDN  37292  hdmapoc  37401  hlhilocv  37427
  Copyright terms: Public domain W3C validator