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

Theorem ralbidva 2890
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 685 . 2  |-  ( ph  ->  ( ( x  e.  A  ->  ps )  <->  ( x  e.  A  ->  ch ) ) )
32ralbidv2 2889 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 367    e. wcel 1823   A.wral 2804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709
This theorem depends on definitions:  df-bi 185  df-an 369  df-ral 2809
This theorem is referenced by:  ralbidv  2893  2ralbidva  2896  raleqbidva  3067  ordunisssuc  4969  poinxp  5052  soinxp  5053  frinxp  5054  fnmptfvd  5966  funimass3  5979  fnnfpeq0  6078  fnsuppresOLD  6107  cocan1  6169  cocan2  6170  isores2  6204  isoini2  6210  ofrfval  6521  ofrfval2  6530  tfindsg2  6669  f1oweALT  6757  fnsuppres  6919  dfsmo2  7010  smores  7015  smores2  7017  ac6sfi  7756  fimaxg  7759  ordunifi  7762  isfinite2  7770  fipreima  7818  supisolem  7923  ordiso2  7932  ordtypelem7  7941  cantnf  8103  cantnfOLD  8125  wemapwe  8130  wemapweOLD  8131  rankval3b  8235  rankonidlem  8237  iscard  8347  acndom  8423  dfac12lem3  8516  kmlem2  8522  cflim2  8634  cfsmolem  8641  ttukeylem6  8885  alephreg  8948  suplem2pr  9420  axsup  9649  sup3  10495  infm3  10497  suprleub  10502  dfinfmr  10515  infmrgelb  10518  ofsubeq0  10528  ofsubge0  10530  zextlt  10933  prime  10939  suprfinzcl  10975  indstr  11151  supxr2  11508  supxrbnd1  11516  supxrbnd2  11517  supxrleub  11521  supxrbnd  11523  infmxrgelb  11529  fzshftral  11770  mptnn0fsupp  12088  swrdeq  12663  swrdspsleq  12668  clim  13402  rlim  13403  clim2  13412  clim2c  13413  clim0c  13415  ello1mpt  13429  lo1o1  13440  o1lo1  13445  climabs0  13493  o1compt  13495  rlimdiv  13553  geomulcvg  13770  mertenslem2  13779  mertens  13780  rpnnen2  14046  sqrt2irr  14069  pc11  14490  pcz  14491  1arith  14532  vdwlem8  14593  vdwlem11  14596  vdw  14599  ramval  14613  pwsle  14984  mrieqvd  15130  mreacs  15150  cidpropd  15201  ismon2  15225  monpropd  15228  isepi  15231  isepi2  15232  subsubc  15344  funcres2b  15388  funcpropd  15391  isfull2  15402  isfth2  15406  fucsect  15463  fucinv  15464  pospropd  15966  ipodrsfi  15995  tsrss  16055  grpidpropd  16090  mndpropd  16148  grppropd  16270  issubg4  16422  gass  16541  gsmsymgrfixlem1  16654  gsmsymgreqlem2  16658  gexdvds  16806  gexdvds2  16807  subgpgp  16819  sylow3lem6  16854  efgval2  16944  efgsp1  16957  dprdf11  17261  dprdf11OLD  17268  subgdmdprd  17279  ringpropd  17428  abvpropd  17689  lsspropd  17861  lbspropd  17943  assapropd  18174  psrbaglefi  18221  psrbaglefiOLD  18222  psrbagconf1o  18224  gsumbagdiaglem  18225  mplmonmul  18324  gsumply1eq  18545  phlpropd  18866  ishil2  18926  lindfmm  19032  islindf4  19043  islindf5  19044  scmatf1  19203  cpmatmcllem  19389  cpmatmcl  19390  decpmataa0  19439  decpmatmulsumfsupp  19444  pmatcollpw2lem  19448  pm2mpmhmlem1  19489  tgss2  19659  isclo  19758  neips  19784  opnnei  19791  isperf3  19824  ssidcn  19926  lmbrf  19931  cnnei  19953  cnrest2  19957  lmss  19969  lmres  19971  ist1-2  20018  ist1-3  20020  isreg2  20048  cmpfi  20078  bwth  20080  1stccn  20133  subislly  20151  kgencn  20226  ptclsg  20285  ptcnplem  20291  xkococnlem  20329  xkoinjcn  20357  tgqtop  20382  qtopcn  20384  fbflim  20646  flimrest  20653  flfnei  20661  isflf  20663  cnflf  20672  fclsopn  20684  fclsbas  20691  fclsrest  20694  isfcf  20704  cnfcf  20712  ptcmplem3  20723  tmdgsum2  20764  eltsms  20800  tsmsgsum  20806  tsmsgsumOLD  20809  tsmssubm  20813  tsmsf1o  20816  utopsnneiplem  20919  ismet2  21005  prdsxmetlem  21040  elmopn2  21117  prdsbl  21163  metss  21180  metrest  21196  metcnp  21213  metcnp2  21214  metcn  21215  metucnOLD  21260  metucn  21261  nrginvrcn  21369  metdsge  21522  divcn  21541  elcncf2  21563  mulc1cncf  21578  cncfmet  21581  evth2  21629  lmmbr2  21867  lmmbrf  21870  iscfil2  21874  cfil3i  21877  iscau2  21885  iscau4  21887  iscauf  21888  caucfil  21891  iscmet3lem3  21898  cfilres  21904  causs  21906  lmclim  21910  rrxmet  22004  evthicc2  22041  cniccbdd  22042  ovolfioo  22048  ovolficc  22049  ismbl2  22107  mbfsup  22240  mbfinf  22241  mbflimsup  22242  0plef  22248  mbfi1flim  22299  xrge0f  22307  itg2mulclem  22322  itgeqa  22389  ellimc2  22450  ellimc3  22452  limcflf  22454  cnlimc  22461  dvferm1  22555  dvferm2  22557  rolle  22560  dvivthlem1  22578  ftc1lem6  22611  itgsubst  22619  mdegle0  22646  deg1leb  22664  plydivex  22862  ulm2  22949  ulmcaulem  22958  ulmcau  22959  ulmdvlem3  22966  abelthlem9  23004  abelth  23005  rlimcnp  23496  ftalem3  23549  issqf  23611  sqf11  23614  dvdsmulf1o  23671  dchrelbas4  23719  dchrinv  23737  2sqlem6  23845  chpo1ubb  23867  dchrmusumlema  23879  dchrisum0lema  23900  ostth3  24024  eqeelen  24412  brbtwn2  24413  colinearalg  24418  axcgrid  24424  axsegconlem1  24425  ax5seglem4  24440  ax5seglem5  24441  axbtwnid  24447  axpasch  24449  axeuclidlem  24470  axcontlem2  24473  axcontlem4  24475  axcontlem7  24478  axcontlem12  24483  wwlknext  24929  clwwlkel  24998  clwwlkf  24999  wwlkext2clwwlk  25008  wwlksubclwwlk  25009  clwlkfclwwlk  25049  extwwlkfablem2  25283  numclwwlkovf2ex  25291  isgrpo2  25400  nmounbi  25892  blocnilem  25920  isph  25938  phoeqi  25974  h2hcau  26097  h2hlm  26098  hial2eq2  26225  hoeq1  26950  hoeq2  26951  adjsym  26953  cnvadj  27012  hhcno  27024  hhcnf  27025  adjvalval  27057  leop2  27244  leoptri  27256  mdbr2  27416  dmdbr2  27423  mddmd2  27429  cdj3lem3b  27560  toslublem  27892  tosglblem  27894  submarchi  27967  isarchi3  27968  cmpcref  28091  lmdvg  28173  eulerpartlemd  28572  subfacp1lem3  28893  subfacp1lem5  28895  dfrdg2  29471  itg2gt0cn  30313  ftc1cnnc  30332  opnrebl  30381  lmclim2  30494  caures  30496  sstotbnd2  30513  rrnmet  30568  rrncmslem  30571  isdrngo3  30605  isidlc  30655  wepwsolem  31229  fnwe2lem2  31239  islnm2  31266  isprm7  31436  caofcan  31472  evthiccabs  31771  ellimcabssub0  31865  climf  31870  clim2f  31884  clim2cf  31898  clim0cf  31902  fourierdlem70  32201  fourierdlem71  32202  fourierdlem73  32204  fourierdlem80  32211  fourierdlem83  32214  fourierdlem87  32218  pfxeq  32651  islinindfis  33323  elbigolo1  33451  aacllem  33623  cvrval2  35415  isat3  35448  iscvlat2N  35465  glbconN  35517  ltrneq  36289  cdlemefrs29clN  36541  cdlemefrs32fva  36542  cdleme32fva  36579  cdlemk33N  37051  cdlemk34  37052  cdlemkid3N  37075  cdlemkid4  37076  diaglbN  37198  dibglbN  37309  dihglbcpreN  37443  dihglblem6  37483  hdmap1eulem  37967  hdmap1eulemOLDN  37968  hdmapoc  38077  hlhilocv  38103
  Copyright terms: Public domain W3C validator