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

Theorem ralbidva 2801
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 2800 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 1872   A.wral 2714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752
This theorem depends on definitions:  df-bi 188  df-an 372  df-ral 2719
This theorem is referenced by:  ralbidv  2804  2ralbidva  2807  raleqbidva  2980  poinxp  4860  soinxp  4861  frinxp  4862  ordunisssuc  5487  fnmptfvd  5944  funimass3  5957  fnnfpeq0  6054  cocan1  6148  cocan2  6149  isores2  6183  isoini2  6189  ofrfval  6497  ofrfval2  6507  tfindsg2  6646  f1oweALT  6735  fnsuppres  6897  dfsmo2  7021  smores  7026  smores2  7028  dfrecs3  7046  ac6sfi  7768  fimaxg  7771  ordunifi  7774  isfinite2  7782  fipreima  7833  supisolem  7942  fiming  7967  infempty  7975  ordiso2  7983  ordtypelem7  7992  cantnf  8150  wemapwe  8154  rankval3b  8249  rankonidlem  8251  iscard  8361  acndom  8433  dfac12lem3  8526  kmlem2  8532  cflim2  8644  cfsmolem  8651  ttukeylem6  8895  alephreg  8958  suplem2pr  9429  axsup  9660  sup3  10517  infm3  10519  suprleub  10524  dfinfre  10539  dfinfmrOLD  10540  infregelb  10545  infmrgelbOLD  10546  ofsubeq0  10557  ofsubge0  10559  zextlt  10961  prime  10967  suprfinzcl  11001  indstr  11178  supxr2  11550  supxrbnd1  11558  supxrbnd2  11559  supxrleub  11563  supxrbnd  11565  infxrgelb  11572  infmxrgelbOLD  11576  fzshftral  11833  mptnn0fsupp  12159  swrdeq  12746  swrdspsleq  12751  clim  13501  rlim  13502  clim2  13511  clim2c  13512  clim0c  13514  ello1mpt  13528  lo1o1  13539  o1lo1  13544  climabs0  13592  o1compt  13594  rlimdiv  13652  geomulcvg  13875  mertenslem2  13884  mertens  13885  rpnnen2  14221  sqrt2irr  14244  fproddvdsd  14313  pc11  14772  pcz  14773  1arith  14814  vdwlem8  14881  vdwlem11  14884  vdw  14887  ramval  14903  ramvalOLD  14904  pwsle  15333  mrieqvd  15487  mreacs  15507  cidpropd  15558  ismon2  15582  monpropd  15585  isepi  15588  isepi2  15589  subsubc  15701  funcres2b  15745  funcpropd  15748  isfull2  15759  isfth2  15763  fucsect  15820  fucinv  15821  pospropd  16323  ipodrsfi  16352  tsrss  16412  grpidpropd  16447  mndpropd  16505  grppropd  16627  issubg4  16779  gass  16898  gsmsymgrfixlem1  17011  gsmsymgreqlem2  17015  gexdvds  17178  gexdvds2  17180  subgpgp  17192  sylow3lem6  17227  efgval2  17317  efgsp1  17330  dprdf11  17599  subgdmdprd  17610  ringpropd  17755  abvpropd  18013  lsspropd  18183  lbspropd  18265  assapropd  18494  psrbaglefi  18539  psrbagconf1o  18541  gsumbagdiaglem  18542  mplmonmul  18631  gsumply1eq  18842  phlpropd  19164  ishil2  19224  lindfmm  19327  islindf4  19338  islindf5  19339  scmatf1  19498  cpmatmcllem  19684  cpmatmcl  19685  decpmataa0  19734  decpmatmulsumfsupp  19739  pmatcollpw2lem  19743  pm2mpmhmlem1  19784  tgss2  19945  isclo  20045  neips  20071  opnnei  20078  isperf3  20111  ssidcn  20213  lmbrf  20218  cnnei  20240  cnrest2  20244  lmss  20256  lmres  20258  ist1-2  20305  ist1-3  20307  isreg2  20335  cmpfi  20365  bwth  20367  1stccn  20420  subislly  20438  kgencn  20513  ptclsg  20572  ptcnplem  20578  xkococnlem  20616  xkoinjcn  20644  tgqtop  20669  qtopcn  20671  fbflim  20933  flimrest  20940  flfnei  20948  isflf  20950  cnflf  20959  fclsopn  20971  fclsbas  20978  fclsrest  20981  isfcf  20991  cnfcf  20999  ptcmplem3  21011  tmdgsum2  21053  eltsms  21089  tsmsgsum  21095  tsmssubm  21099  tsmsf1o  21101  utopsnneiplem  21204  ismet2  21290  prdsxmetlem  21325  elmopn2  21402  prdsbl  21448  metss  21465  metrest  21481  metcnp  21498  metcnp2  21499  metcn  21500  metucn  21528  nrginvrcn  21636  metdsge  21808  metdsgeOLD  21823  divcn  21842  elcncf2  21864  mulc1cncf  21879  cncfmet  21882  evth2  21930  lmmbr2  22171  lmmbrf  22174  iscfil2  22178  cfil3i  22181  iscau2  22189  iscau4  22191  iscauf  22192  caucfil  22195  iscmet3lem3  22202  cfilres  22208  causs  22210  lmclim  22214  rrxmet  22304  evthicc2  22353  cniccbdd  22354  ovolfioo  22362  ovolficc  22363  ismbl2  22423  mbfsup  22562  mbfinf  22563  mbfinfOLD  22564  mbflimsup  22565  mbflimsupOLD  22566  0plef  22572  mbfi1flim  22623  xrge0f  22631  itg2mulclem  22646  itgeqa  22713  ellimc2  22774  ellimc3  22776  limcflf  22778  cnlimc  22785  dvferm1  22879  dvferm2  22881  rolle  22884  dvivthlem1  22902  ftc1lem6  22935  itgsubst  22943  mdegle0  22968  deg1leb  22986  plydivex  23192  ulm2  23282  ulmcaulem  23291  ulmcau  23292  ulmdvlem3  23299  abelthlem9  23337  abelth  23338  rlimcnp  23833  ftalem3  23941  issqf  24005  sqf11  24008  dvdsmulf1o  24065  dchrelbas4  24113  dchrinv  24131  2sqlem6  24239  chpo1ubb  24261  dchrmusumlema  24273  dchrisum0lema  24294  ostth3  24418  tgcgr4  24518  eqeelen  24876  brbtwn2  24877  colinearalg  24882  axcgrid  24888  axsegconlem1  24889  ax5seglem4  24904  ax5seglem5  24905  axbtwnid  24911  axpasch  24913  axeuclidlem  24934  axcontlem2  24937  axcontlem4  24939  axcontlem7  24942  axcontlem12  24947  wwlknext  25394  clwwlkel  25463  clwwlkf  25464  wwlkext2clwwlk  25473  wwlksubclwwlk  25474  clwlkfclwwlk  25514  extwwlkfablem2  25748  numclwwlkovf2ex  25756  isgrpo2  25867  nmounbi  26359  blocnilem  26387  isph  26405  phoeqi  26441  h2hcau  26574  h2hlm  26575  hial2eq2  26702  hoeq1  27425  hoeq2  27426  adjsym  27428  cnvadj  27487  hhcno  27499  hhcnf  27500  adjvalval  27532  leop2  27719  leoptri  27731  mdbr2  27891  dmdbr2  27898  mddmd2  27904  cdj3lem3b  28035  infxrge0gelb  28300  infxrge0gelbOLD  28301  toslublem  28379  tosglblem  28381  submarchi  28454  isarchi3  28455  cmpcref  28629  lmdvg  28711  eulerpartlemd  29151  subfacp1lem3  29857  subfacp1lem5  29859  dfrdg2  30393  opnrebl  30925  poimirlem23  31870  broucube  31881  itg2gt0cn  31904  ftc1cnnc  31923  lmclim2  31994  caures  31996  sstotbnd2  32013  rrnmet  32068  rrncmslem  32071  isdrngo3  32105  isidlc  32155  cvrval2  32752  isat3  32785  iscvlat2N  32802  glbconN  32854  ltrneq  33626  cdlemefrs29clN  33878  cdlemefrs32fva  33879  cdleme32fva  33916  cdlemk33N  34388  cdlemk34  34389  cdlemkid3N  34412  cdlemkid4  34413  diaglbN  34535  dibglbN  34646  dihglbcpreN  34780  dihglblem6  34820  hdmap1eulem  35304  hdmap1eulemOLDN  35305  hdmapoc  35414  hlhilocv  35440  wepwsolem  35813  fnwe2lem2  35822  islnm2  35849  isprm7  36573  caofcan  36585  evthiccabs  37485  ellimcabssub0  37580  climf  37585  clim2f  37599  clim2cf  37614  clim0cf  37618  fourierdlem70  37923  fourierdlem71  37924  fourierdlem73  37926  fourierdlem80  37933  fourierdlem83  37936  fourierdlem87  37940  hoidmv1lelem3  38262  hoidmvlelem4  38267  hoidmvlelem5  38268  pfxeq  38758  isuvtxa  39207  uvtx2vtx1edg  39211  uvtx2vtx1edgb  39212  iscplgrnb  39222  iscplgredg  39223  islinindfis  39845  elbigolo1  39971  aacllem  40143
  Copyright terms: Public domain W3C validator