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

Theorem ralbidva 3172
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 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
ralbidva (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralbidva
StepHypRef Expression
1 ralbidva.1 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
21pm5.74da 829 . 2 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
32ralbidv2 3171 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  wcel 2158  wral 3095
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004
This theorem depends on definitions:  df-bi 198  df-an 385  df-ral 3100
This theorem is referenced by:  ralbidv  3173  2ralbidva  3175  raleqbidva  3342  poinxp  5381  soinxp  5382  frinxp  5383  ordunisssuc  6040  fnmptfvd  6539  funimass3  6552  fnnfpeq0  6666  cocan1  6767  cocan2  6768  isores2  6804  isoini2  6810  ofrfval  7132  ofrfval2  7142  tfindsg2  7288  f1oweALT  7379  fnsuppres  7554  dfsmo2  7677  smores  7682  smores2  7684  dfrecs3  7702  ac6sfi  8440  fimaxg  8443  ordunifi  8446  isfinite2  8454  fipreima  8508  supisolem  8615  fiming  8640  infempty  8648  ordiso2  8656  ordtypelem7  8665  cantnf  8834  wemapwe  8838  rankval3b  8933  rankonidlem  8935  iscard  9081  acndom  9154  dfac12lem3  9249  kmlem2  9255  cflim2  9367  cfsmolem  9374  ttukeylem6  9618  alephreg  9686  suplem2pr  10157  axsup  10395  sup3  11262  infm3  11264  suprleub  11271  dfinfre  11286  infregelb  11289  ofsubeq0  11299  ofsubge0  11301  zextlt  11713  prime  11720  suprfinzcl  11754  indstr  11971  supxr2  12358  supxrbnd1  12365  supxrbnd2  12366  supxrleub  12370  supxrbnd  12372  infxrgelb  12379  fzshftral  12647  mptnn0fsupp  13016  swrdeq  13664  swrdspsleq  13669  clim  14444  rlim  14445  clim2  14454  clim2c  14455  clim0c  14457  ello1mpt  14471  lo1o1  14482  o1lo1  14487  climabs0  14535  o1compt  14537  rlimdiv  14595  geomulcvg  14825  mertenslem2  14834  mertens  14835  rpnnen2lem12  15170  sqrt2irr  15195  fprodfvdvdsd  15274  fproddvdsd  15275  dfgcd2  15478  isprm7  15633  pc11  15797  pcz  15798  1arith  15844  vdwlem8  15905  vdwlem11  15908  vdw  15911  ramval  15925  pwsle  16353  mrieqvd  16499  mreacs  16519  cidpropd  16570  ismon2  16594  monpropd  16597  isepi  16600  isepi2  16601  subsubc  16713  funcres2b  16757  funcpropd  16760  isfull2  16771  isfth2  16775  fucsect  16832  fucinv  16833  pospropd  17335  ipodrsfi  17364  tsrss  17424  grpidpropd  17462  mndpropd  17517  grppropd  17638  issubg4  17811  gass  17931  gsmsymgrfixlem1  18044  gsmsymgreqlem2  18048  gexdvds  18196  gexdvds2  18197  subgpgp  18209  sylow3lem6  18244  efgval2  18334  efgsp1  18347  dprdf11  18620  subgdmdprd  18631  ringpropd  18780  abvpropd  19042  lsspropd  19220  lbspropd  19302  assapropd  19532  psrbaglefi  19577  psrbagconf1o  19579  gsumbagdiaglem  19580  mplmonmul  19669  gsumply1eq  19879  phlpropd  20206  ishil2  20269  lindfmm  20372  islindf4  20383  islindf5  20384  scmatf1  20544  cpmatmcllem  20732  cpmatmcl  20733  decpmataa0  20782  decpmatmulsumfsupp  20787  pmatcollpw2lem  20791  pm2mpmhmlem1  20832  tgss2  21001  isclo  21101  neips  21127  opnnei  21134  isperf3  21167  ssidcn  21269  lmbrf  21274  cnnei  21296  cnrest2  21300  lmss  21312  lmres  21314  ist1-2  21361  ist1-3  21363  isreg2  21391  cmpfi  21421  bwth  21423  1stccn  21476  subislly  21494  kgencn  21569  ptclsg  21628  ptcnplem  21634  xkococnlem  21672  xkoinjcn  21700  tgqtop  21725  qtopcn  21727  fbflim  21989  flimrest  21996  flfnei  22004  isflf  22006  cnflf  22015  fclsopn  22027  fclsbas  22034  fclsrest  22037  isfcf  22047  cnfcf  22055  ptcmplem3  22067  tmdgsum2  22109  eltsms  22145  tsmsgsum  22151  tsmssubm  22155  tsmsf1o  22157  utopsnneiplem  22260  ismet2  22347  prdsxmetlem  22382  elmopn2  22459  prdsbl  22505  metss  22522  metrest  22538  metcnp  22555  metcnp2  22556  metcn  22557  metucn  22585  nrginvrcn  22705  metdsge  22861  divcn  22880  elcncf2  22902  mulc1cncf  22917  cncfmet  22920  evth2  22968  lmmbr2  23265  lmmbrf  23268  iscfil2  23272  cfil3i  23275  iscau2  23283  iscau4  23285  iscauf  23286  caucfil  23289  iscmet3lem3  23296  cfilres  23302  causs  23304  lmclim  23309  rrxmet  23399  evthicc2  23437  cniccbdd  23438  ovolfioo  23444  ovolficc  23445  ismbl2  23504  mbfsup  23641  mbfinf  23642  mbflimsup  23643  0plef  23649  mbfi1flim  23700  xrge0f  23708  itg2mulclem  23723  itgeqa  23790  ellimc2  23851  ellimc3  23853  limcflf  23855  cnlimc  23862  dvferm1  23958  dvferm2  23960  rolle  23963  dvivthlem1  23981  ftc1lem6  24014  itgsubst  24022  mdegle0  24047  deg1leb  24065  plydivex  24262  ulm2  24349  ulmcaulem  24358  ulmcau  24359  ulmdvlem3  24366  abelthlem9  24404  abelth  24405  rlimcnp  24902  ftalem3  25011  issqf  25072  sqf11  25075  dvdsmulf1o  25130  dchrelbas4  25178  dchrinv  25196  2sqlem6  25358  chpo1ubb  25380  dchrmusumlema  25392  dchrisum0lema  25413  ostth3  25537  tgcgr4  25636  eqeelen  25994  brbtwn2  25995  colinearalg  26000  axcgrid  26006  axsegconlem1  26007  ax5seglem4  26022  ax5seglem5  26023  axbtwnid  26029  axpasch  26031  axeuclidlem  26052  axcontlem2  26055  axcontlem4  26057  axcontlem7  26060  axcontlem12  26065  isuvtx  26511  isuvtxaOLD  26512  uvtx2vtx1edg  26517  uvtx2vtx1edgb  26518  iscplgrnb  26536  iscplgredg  26537  vdiscusgrb  26650  uhgrvd00  26654  upgriswlk  26761  wwlksnext  27026  clwwlkinwwlk  27185  clwwlkel  27191  clwwlkf  27192  clwwlkwwlksb  27200  wwlksext2clwwlk  27203  wwlksext2clwwlkOLD  27204  wwlksubclwwlk  27205  clwlksfclwwlkOLD  27232  clwwlknonex2lem2  27273  nmounbi  27956  blocnilem  27984  isph  28002  phoeqi  28038  h2hcau  28161  h2hlm  28162  hial2eq2  28289  hoeq1  29014  hoeq2  29015  adjsym  29017  cnvadj  29076  hhcno  29088  hhcnf  29089  adjvalval  29121  leop2  29308  leoptri  29320  mdbr2  29480  dmdbr2  29487  mddmd2  29493  cdj3lem3b  29624  infxrge0gelb  29855  toslublem  29989  tosglblem  29991  submarchi  30062  isarchi3  30063  cmpcref  30239  lmdvg  30321  prodindf  30407  eulerpartlemd  30750  subfacp1lem3  31484  subfacp1lem5  31486  dfrdg2  32018  sltrec  32242  opnrebl  32633  poimirlem23  33742  broucube  33753  itg2gt0cn  33774  ftc1cnnc  33793  lmclim2  33862  caures  33864  sstotbnd2  33881  rrnmet  33936  rrncmslem  33939  isdrngo3  34066  isidlc  34122  cvrval2  35051  isat3  35084  iscvlat2N  35101  glbconN  35154  ltrneq  35926  cdlemefrs29clN  36177  cdlemefrs32fva  36178  cdleme32fva  36215  cdlemk33N  36687  cdlemk34  36688  cdlemkid3N  36711  cdlemkid4  36712  diaglbN  36833  dibglbN  36944  dihglbcpreN  37078  dihglblem6  37118  hdmap1eulem  37600  hdmap1eulemOLDN  37601  hdmapoc  37709  hlhilocv  37735  wepwsolem  38110  fnwe2lem2  38119  islnm2  38146  clsk3nimkb  38835  ntrclsneine0  38860  ntrneineine0  38882  ntrneineine1  38883  ntrneicls00  38884  ntrneicls11  38885  ntrneiiso  38886  ntrneik2  38887  ntrneix2  38888  ntrneikb  38889  ntrneixb  38890  ntrneik3  38891  ntrneix3  38892  ntrneik13  38893  ntrneix13  38894  ntrneik4w  38895  ntrneik4  38896  caofcan  39019  infxrbnd2  40062  supminfxr  40170  evthiccabs  40199  ellimcabssub0  40326  climf  40331  clim2f  40345  clim2cf  40359  clim0cf  40363  limsupmnflem  40429  limsupre2lem  40433  limsupreuzmpt  40448  supcnvlimsup  40449  limsupge  40470  liminfreuzlem  40511  liminfltlem  40513  liminflimsupclim  40516  fourierdlem70  40869  fourierdlem71  40870  fourierdlem73  40872  fourierdlem80  40879  fourierdlem83  40882  fourierdlem87  40886  voliunsge0lem  41165  meaiuninclem  41173  meaiuninc3v  41177  hoidmv1lelem3  41286  hoidmvlelem4  41291  hoidmvlelem5  41292  issmflem  41415  pfxeq  41976  islinindfis  42803  elbigolo1  42916  aacllem  43115
  Copyright terms: Public domain W3C validator