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

Theorem ralbidva 2836
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 698 . 2  |-  ( ph  ->  ( ( x  e.  A  ->  ps )  <->  ( x  e.  A  ->  ch ) ) )
32ralbidv2 2835 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375    e. wcel 1898   A.wral 2749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769
This theorem depends on definitions:  df-bi 190  df-an 377  df-ral 2754
This theorem is referenced by:  ralbidv  2839  2ralbidva  2842  raleqbidva  3015  poinxp  4917  soinxp  4918  frinxp  4919  ordunisssuc  5544  fnmptfvd  6008  funimass3  6021  fnnfpeq0  6119  cocan1  6214  cocan2  6215  isores2  6249  isoini2  6255  ofrfval  6566  ofrfval2  6576  tfindsg2  6715  f1oweALT  6804  fnsuppres  6969  dfsmo2  7092  smores  7097  smores2  7099  dfrecs3  7117  ac6sfi  7841  fimaxg  7844  ordunifi  7847  isfinite2  7855  fipreima  7906  supisolem  8015  fiming  8040  infempty  8048  ordiso2  8056  ordtypelem7  8065  cantnf  8224  wemapwe  8228  rankval3b  8323  rankonidlem  8325  iscard  8435  acndom  8508  dfac12lem3  8601  kmlem2  8607  cflim2  8719  cfsmolem  8726  ttukeylem6  8970  alephreg  9033  suplem2pr  9504  axsup  9735  sup3  10594  infm3  10596  suprleub  10601  dfinfre  10616  dfinfmrOLD  10617  infregelb  10622  infmrgelbOLD  10623  ofsubeq0  10634  ofsubge0  10636  zextlt  11039  prime  11045  suprfinzcl  11079  indstr  11256  supxr2  11628  supxrbnd1  11636  supxrbnd2  11637  supxrleub  11641  supxrbnd  11643  infxrgelb  11650  infmxrgelbOLD  11654  fzshftral  11911  mptnn0fsupp  12241  swrdeq  12837  swrdspsleq  12842  clim  13607  rlim  13608  clim2  13617  clim2c  13618  clim0c  13620  ello1mpt  13634  lo1o1  13645  o1lo1  13650  climabs0  13698  o1compt  13700  rlimdiv  13758  geomulcvg  13981  mertenslem2  13990  mertens  13991  rpnnen2  14327  sqrt2irr  14350  fproddvdsd  14419  pc11  14878  pcz  14879  1arith  14920  vdwlem8  14987  vdwlem11  14990  vdw  14993  ramval  15009  ramvalOLD  15010  pwsle  15439  mrieqvd  15593  mreacs  15613  cidpropd  15664  ismon2  15688  monpropd  15691  isepi  15694  isepi2  15695  subsubc  15807  funcres2b  15851  funcpropd  15854  isfull2  15865  isfth2  15869  fucsect  15926  fucinv  15927  pospropd  16429  ipodrsfi  16458  tsrss  16518  grpidpropd  16553  mndpropd  16611  grppropd  16733  issubg4  16885  gass  17004  gsmsymgrfixlem1  17117  gsmsymgreqlem2  17121  gexdvds  17284  gexdvds2  17286  subgpgp  17298  sylow3lem6  17333  efgval2  17423  efgsp1  17436  dprdf11  17705  subgdmdprd  17716  ringpropd  17861  abvpropd  18119  lsspropd  18289  lbspropd  18371  assapropd  18600  psrbaglefi  18645  psrbagconf1o  18647  gsumbagdiaglem  18648  mplmonmul  18737  gsumply1eq  18948  phlpropd  19271  ishil2  19331  lindfmm  19434  islindf4  19445  islindf5  19446  scmatf1  19605  cpmatmcllem  19791  cpmatmcl  19792  decpmataa0  19841  decpmatmulsumfsupp  19846  pmatcollpw2lem  19850  pm2mpmhmlem1  19891  tgss2  20052  isclo  20152  neips  20178  opnnei  20185  isperf3  20218  ssidcn  20320  lmbrf  20325  cnnei  20347  cnrest2  20351  lmss  20363  lmres  20365  ist1-2  20412  ist1-3  20414  isreg2  20442  cmpfi  20472  bwth  20474  1stccn  20527  subislly  20545  kgencn  20620  ptclsg  20679  ptcnplem  20685  xkococnlem  20723  xkoinjcn  20751  tgqtop  20776  qtopcn  20778  fbflim  21040  flimrest  21047  flfnei  21055  isflf  21057  cnflf  21066  fclsopn  21078  fclsbas  21085  fclsrest  21088  isfcf  21098  cnfcf  21106  ptcmplem3  21118  tmdgsum2  21160  eltsms  21196  tsmsgsum  21202  tsmssubm  21206  tsmsf1o  21208  utopsnneiplem  21311  ismet2  21397  prdsxmetlem  21432  elmopn2  21509  prdsbl  21555  metss  21572  metrest  21588  metcnp  21605  metcnp2  21606  metcn  21607  metucn  21635  nrginvrcn  21743  metdsge  21915  metdsgeOLD  21930  divcn  21949  elcncf2  21971  mulc1cncf  21986  cncfmet  21989  evth2  22037  lmmbr2  22278  lmmbrf  22281  iscfil2  22285  cfil3i  22288  iscau2  22296  iscau4  22298  iscauf  22299  caucfil  22302  iscmet3lem3  22309  cfilres  22315  causs  22317  lmclim  22321  rrxmet  22411  evthicc2  22460  cniccbdd  22461  ovolfioo  22469  ovolficc  22470  ismbl2  22530  mbfsup  22669  mbfinf  22670  mbfinfOLD  22671  mbflimsup  22672  mbflimsupOLD  22673  0plef  22679  mbfi1flim  22730  xrge0f  22738  itg2mulclem  22753  itgeqa  22820  ellimc2  22881  ellimc3  22883  limcflf  22885  cnlimc  22892  dvferm1  22986  dvferm2  22988  rolle  22991  dvivthlem1  23009  ftc1lem6  23042  itgsubst  23050  mdegle0  23075  deg1leb  23093  plydivex  23299  ulm2  23389  ulmcaulem  23398  ulmcau  23399  ulmdvlem3  23406  abelthlem9  23444  abelth  23445  rlimcnp  23940  ftalem3  24048  issqf  24112  sqf11  24115  dvdsmulf1o  24172  dchrelbas4  24220  dchrinv  24238  2sqlem6  24346  chpo1ubb  24368  dchrmusumlema  24380  dchrisum0lema  24401  ostth3  24525  tgcgr4  24625  eqeelen  24983  brbtwn2  24984  colinearalg  24989  axcgrid  24995  axsegconlem1  24996  ax5seglem4  25011  ax5seglem5  25012  axbtwnid  25018  axpasch  25020  axeuclidlem  25041  axcontlem2  25044  axcontlem4  25046  axcontlem7  25049  axcontlem12  25054  wwlknext  25501  clwwlkel  25570  clwwlkf  25571  wwlkext2clwwlk  25580  wwlksubclwwlk  25581  clwlkfclwwlk  25621  extwwlkfablem2  25855  numclwwlkovf2ex  25863  isgrpo2  25974  nmounbi  26466  blocnilem  26494  isph  26512  phoeqi  26548  h2hcau  26681  h2hlm  26682  hial2eq2  26809  hoeq1  27532  hoeq2  27533  adjsym  27535  cnvadj  27594  hhcno  27606  hhcnf  27607  adjvalval  27639  leop2  27826  leoptri  27838  mdbr2  27998  dmdbr2  28005  mddmd2  28011  cdj3lem3b  28142  infxrge0gelb  28399  infxrge0gelbOLD  28400  toslublem  28477  tosglblem  28479  submarchi  28552  isarchi3  28553  cmpcref  28726  lmdvg  28808  eulerpartlemd  29248  subfacp1lem3  29954  subfacp1lem5  29956  dfrdg2  30491  opnrebl  31025  poimirlem23  32008  broucube  32019  itg2gt0cn  32042  ftc1cnnc  32061  lmclim2  32132  caures  32134  sstotbnd2  32151  rrnmet  32206  rrncmslem  32209  isdrngo3  32243  isidlc  32293  cvrval2  32885  isat3  32918  iscvlat2N  32935  glbconN  32987  ltrneq  33759  cdlemefrs29clN  34011  cdlemefrs32fva  34012  cdleme32fva  34049  cdlemk33N  34521  cdlemk34  34522  cdlemkid3N  34545  cdlemkid4  34546  diaglbN  34668  dibglbN  34779  dihglbcpreN  34913  dihglblem6  34953  hdmap1eulem  35437  hdmap1eulemOLDN  35438  hdmapoc  35547  hlhilocv  35573  wepwsolem  35945  fnwe2lem2  35954  islnm2  35981  isprm7  36704  caofcan  36716  evthiccabs  37631  ellimcabssub0  37735  climf  37740  clim2f  37754  clim2cf  37769  clim0cf  37773  fourierdlem70  38078  fourierdlem71  38079  fourierdlem73  38081  fourierdlem80  38088  fourierdlem83  38091  fourierdlem87  38095  hoidmv1lelem3  38453  hoidmvlelem4  38458  hoidmvlelem5  38459  pfxeq  38985  isuvtxa  39517  uvtx2vtx1edg  39521  uvtx2vtx1edgb  39522  iscplgrnb  39534  iscplgredg  39535  vdiscusgrb  39617  uhgrvd00  39621  islinindfis  40515  elbigolo1  40641  aacllem  40813
  Copyright terms: Public domain W3C validator