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

Theorem ralbidva 2868
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 691 . 2  |-  ( ph  ->  ( ( x  e.  A  ->  ps )  <->  ( x  e.  A  ->  ch ) ) )
32ralbidv2 2867 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    e. wcel 1870   A.wral 2782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751
This theorem depends on definitions:  df-bi 188  df-an 372  df-ral 2787
This theorem is referenced by:  ralbidv  2871  2ralbidva  2874  raleqbidva  3048  poinxp  4918  soinxp  4919  frinxp  4920  ordunisssuc  5544  fnmptfvd  6000  funimass3  6013  fnnfpeq0  6110  cocan1  6204  cocan2  6205  isores2  6239  isoini2  6245  ofrfval  6553  ofrfval2  6563  tfindsg2  6702  f1oweALT  6791  fnsuppres  6953  dfsmo2  7074  smores  7079  smores2  7081  dfrecs3  7099  ac6sfi  7821  fimaxg  7824  ordunifi  7827  isfinite2  7835  fipreima  7886  supisolem  7995  infempty  8022  ordiso2  8030  ordtypelem7  8039  cantnf  8197  wemapwe  8201  rankval3b  8296  rankonidlem  8298  iscard  8408  acndom  8480  dfac12lem3  8573  kmlem2  8579  cflim2  8691  cfsmolem  8698  ttukeylem6  8942  alephreg  9005  suplem2pr  9477  axsup  9708  sup3  10566  infm3  10568  suprleub  10573  dfinfre  10588  dfinfmrOLD  10589  infregelb  10594  infmrgelbOLD  10595  ofsubeq0  10606  ofsubge0  10608  zextlt  11010  prime  11016  suprfinzcl  11050  indstr  11227  supxr2  11599  supxrbnd1  11607  supxrbnd2  11608  supxrleub  11612  supxrbnd  11614  infxrgelb  11621  infmxrgelbOLD  11625  fzshftral  11880  mptnn0fsupp  12206  swrdeq  12785  swrdspsleq  12790  clim  13536  rlim  13537  clim2  13546  clim2c  13547  clim0c  13549  ello1mpt  13563  lo1o1  13574  o1lo1  13579  climabs0  13627  o1compt  13629  rlimdiv  13687  geomulcvg  13910  mertenslem2  13919  mertens  13920  rpnnen2  14256  sqrt2irr  14279  fproddvdsd  14348  pc11  14792  pcz  14793  1arith  14834  vdwlem8  14901  vdwlem11  14904  vdw  14907  ramval  14923  ramvalOLD  14924  pwsle  15349  mrieqvd  15495  mreacs  15515  cidpropd  15566  ismon2  15590  monpropd  15593  isepi  15596  isepi2  15597  subsubc  15709  funcres2b  15753  funcpropd  15756  isfull2  15767  isfth2  15771  fucsect  15828  fucinv  15829  pospropd  16331  ipodrsfi  16360  tsrss  16420  grpidpropd  16455  mndpropd  16513  grppropd  16635  issubg4  16787  gass  16906  gsmsymgrfixlem1  17019  gsmsymgreqlem2  17023  gexdvds  17171  gexdvds2  17172  subgpgp  17184  sylow3lem6  17219  efgval2  17309  efgsp1  17322  dprdf11  17591  subgdmdprd  17602  ringpropd  17747  abvpropd  18005  lsspropd  18175  lbspropd  18257  assapropd  18486  psrbaglefi  18531  psrbagconf1o  18533  gsumbagdiaglem  18534  mplmonmul  18623  gsumply1eq  18834  phlpropd  19153  ishil2  19213  lindfmm  19316  islindf4  19327  islindf5  19328  scmatf1  19487  cpmatmcllem  19673  cpmatmcl  19674  decpmataa0  19723  decpmatmulsumfsupp  19728  pmatcollpw2lem  19732  pm2mpmhmlem1  19773  tgss2  19934  isclo  20034  neips  20060  opnnei  20067  isperf3  20100  ssidcn  20202  lmbrf  20207  cnnei  20229  cnrest2  20233  lmss  20245  lmres  20247  ist1-2  20294  ist1-3  20296  isreg2  20324  cmpfi  20354  bwth  20356  1stccn  20409  subislly  20427  kgencn  20502  ptclsg  20561  ptcnplem  20567  xkococnlem  20605  xkoinjcn  20633  tgqtop  20658  qtopcn  20660  fbflim  20922  flimrest  20929  flfnei  20937  isflf  20939  cnflf  20948  fclsopn  20960  fclsbas  20967  fclsrest  20970  isfcf  20980  cnfcf  20988  ptcmplem3  21000  tmdgsum2  21042  eltsms  21078  tsmsgsum  21084  tsmssubm  21088  tsmsf1o  21090  utopsnneiplem  21193  ismet2  21279  prdsxmetlem  21314  elmopn2  21391  prdsbl  21437  metss  21454  metrest  21470  metcnp  21487  metcnp2  21488  metcn  21489  metucn  21517  nrginvrcn  21625  metdsge  21777  divcn  21796  elcncf2  21818  mulc1cncf  21833  cncfmet  21836  evth2  21884  lmmbr2  22122  lmmbrf  22125  iscfil2  22129  cfil3i  22132  iscau2  22140  iscau4  22142  iscauf  22143  caucfil  22146  iscmet3lem3  22153  cfilres  22159  causs  22161  lmclim  22165  rrxmet  22255  evthicc2  22292  cniccbdd  22293  ovolfioo  22299  ovolficc  22300  ismbl2  22358  mbfsup  22497  mbfinf  22498  mbfinfOLD  22499  mbflimsup  22500  mbflimsupOLD  22501  0plef  22507  mbfi1flim  22558  xrge0f  22566  itg2mulclem  22581  itgeqa  22648  ellimc2  22709  ellimc3  22711  limcflf  22713  cnlimc  22720  dvferm1  22814  dvferm2  22816  rolle  22819  dvivthlem1  22837  ftc1lem6  22870  itgsubst  22878  mdegle0  22903  deg1leb  22921  plydivex  23118  ulm2  23205  ulmcaulem  23214  ulmcau  23215  ulmdvlem3  23222  abelthlem9  23260  abelth  23261  rlimcnp  23756  ftalem3  23864  issqf  23926  sqf11  23929  dvdsmulf1o  23986  dchrelbas4  24034  dchrinv  24052  2sqlem6  24160  chpo1ubb  24182  dchrmusumlema  24194  dchrisum0lema  24215  ostth3  24339  eqeelen  24780  brbtwn2  24781  colinearalg  24786  axcgrid  24792  axsegconlem1  24793  ax5seglem4  24808  ax5seglem5  24809  axbtwnid  24815  axpasch  24817  axeuclidlem  24838  axcontlem2  24841  axcontlem4  24843  axcontlem7  24846  axcontlem12  24851  wwlknext  25297  clwwlkel  25366  clwwlkf  25367  wwlkext2clwwlk  25376  wwlksubclwwlk  25377  clwlkfclwwlk  25417  extwwlkfablem2  25651  numclwwlkovf2ex  25659  isgrpo2  25770  nmounbi  26262  blocnilem  26290  isph  26308  phoeqi  26344  h2hcau  26467  h2hlm  26468  hial2eq2  26595  hoeq1  27318  hoeq2  27319  adjsym  27321  cnvadj  27380  hhcno  27392  hhcnf  27393  adjvalval  27425  leop2  27612  leoptri  27624  mdbr2  27784  dmdbr2  27791  mddmd2  27797  cdj3lem3b  27928  infxrge0gelb  28187  toslublem  28266  tosglblem  28268  submarchi  28341  isarchi3  28342  cmpcref  28516  lmdvg  28598  eulerpartlemd  29025  subfacp1lem3  29693  subfacp1lem5  29695  dfrdg2  30229  opnrebl  30761  poimirlem23  31666  broucube  31677  itg2gt0cn  31700  ftc1cnnc  31719  lmclim2  31790  caures  31792  sstotbnd2  31809  rrnmet  31864  rrncmslem  31867  isdrngo3  31901  isidlc  31951  cvrval2  32548  isat3  32581  iscvlat2N  32598  glbconN  32650  ltrneq  33422  cdlemefrs29clN  33674  cdlemefrs32fva  33675  cdleme32fva  33712  cdlemk33N  34184  cdlemk34  34185  cdlemkid3N  34208  cdlemkid4  34209  diaglbN  34331  dibglbN  34442  dihglbcpreN  34576  dihglblem6  34616  hdmap1eulem  35100  hdmap1eulemOLDN  35101  hdmapoc  35210  hlhilocv  35236  wepwsolem  35605  fnwe2lem2  35614  islnm2  35641  isprm7  36296  caofcan  36308  evthiccabs  37177  ellimcabssub0  37268  climf  37273  clim2f  37287  clim2cf  37302  clim0cf  37306  fourierdlem70  37607  fourierdlem71  37608  fourierdlem73  37610  fourierdlem80  37617  fourierdlem83  37620  fourierdlem87  37624  pfxeq  38334  islinindfis  39001  elbigolo1  39128  aacllem  39300
  Copyright terms: Public domain W3C validator