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

Theorem ralbidva 3161
 Description: Formula-building rule for restricted universal quantifier (deduction form). (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 803 . 2 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
32ralbidv2 3160 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∈ wcel 2111  ∀wral 3106 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911 This theorem depends on definitions:  df-bi 210  df-an 400  df-ral 3111 This theorem is referenced by:  ralbidv  3162  2ralbidva  3163  raleqbidva  3370  poinxp  5597  soinxp  5598  frinxp  5599  ordunisssuc  6264  fnmptfvd  6793  funimass3  6806  fnnfpeq0  6922  cocan1  7030  cocan2  7031  isores2  7070  isoini2  7076  ofrfval  7403  ofrfval2  7414  tfindsg2  7563  f1oweALT  7662  fnsuppres  7847  dfsmo2  7974  smores  7979  smores2  7981  dfrecs3  7999  ac6sfi  8753  fimaxg  8756  ordunifi  8759  isfinite2  8767  fipreima  8821  supisolem  8928  fiming  8953  infempty  8962  ordiso2  8970  ordtypelem7  8979  cantnf  9147  wemapwe  9151  rankval3b  9246  rankonidlem  9248  iscard  9395  acndom  9469  dfac12lem3  9563  kmlem2  9569  cflim2  9681  cfsmolem  9688  ttukeylem6  9932  alephreg  10000  suplem2pr  10471  axsup  10712  sup3  11592  infm3  11594  suprleub  11601  dfinfre  11616  infregelb  11619  ofsubeq0  11629  ofsubge0  11631  zextlt  12051  prime  12058  suprfinzcl  12092  indstr  12311  supxr2  12702  supxrbnd1  12709  supxrbnd2  12710  supxrleub  12714  supxrbnd  12716  infxrgelb  12723  fzshftral  12997  mptnn0fsupp  13367  swrdspsleq  14025  pfxeq  14056  clim  14850  rlim  14851  clim2  14860  clim2c  14861  clim0c  14863  ello1mpt  14877  lo1o1  14888  o1lo1  14893  climabs0  14941  o1compt  14943  rlimdiv  15001  geomulcvg  15231  mertenslem2  15240  mertens  15241  rpnnen2lem12  15577  sqrt2irr  15601  fprodfvdvdsd  15682  fproddvdsd  15683  dfgcd2  15891  isprm7  16049  pc11  16213  pcz  16214  1arith  16260  vdwlem8  16321  vdwlem11  16324  vdw  16327  ramval  16341  pwsle  16764  mrieqvd  16908  mreacs  16928  cidpropd  16979  ismon2  17003  monpropd  17006  isepi  17009  isepi2  17010  subsubc  17122  funcres2b  17166  funcpropd  17169  isfull2  17180  isfth2  17184  fucsect  17241  fucinv  17242  pospropd  17743  ipodrsfi  17772  tsrss  17832  grpidpropd  17871  mndpropd  17935  smndex1mnd  18074  grppropd  18118  issubg4  18298  gass  18431  gsmsymgrfixlem1  18555  gsmsymgreqlem2  18559  gexdvds  18709  gexdvds2  18710  subgpgp  18722  sylow3lem6  18757  efgval2  18850  efgsp1  18863  dprdf11  19146  subgdmdprd  19157  ringpropd  19336  abvpropd  19614  lsspropd  19790  lbspropd  19872  phlpropd  20353  ishil2  20417  frlmplusgvalb  20467  frlmvscavalb  20468  frlmvplusgscavalb  20469  lindfmm  20525  islindf4  20536  islindf5  20537  assapropd  20567  psrbaglefi  20620  psrbagconf1o  20622  gsumbagdiaglem  20623  mplmonmul  20716  gsumply1eq  20948  scmatf1  21150  cpmatmcllem  21337  cpmatmcl  21338  decpmataa0  21387  decpmatmulsumfsupp  21392  pmatcollpw2lem  21396  pm2mpmhmlem1  21437  tgss2  21606  isclo  21706  neips  21732  opnnei  21739  isperf3  21772  ssidcn  21874  lmbrf  21879  cnnei  21901  cnrest2  21905  lmss  21917  lmres  21919  ist1-2  21966  ist1-3  21968  isreg2  21996  cmpfi  22027  bwth  22029  1stccn  22082  subislly  22100  kgencn  22175  ptclsg  22234  ptcnplem  22240  xkococnlem  22278  xkoinjcn  22306  tgqtop  22331  qtopcn  22333  fbflim  22595  flimrest  22602  flfnei  22610  isflf  22612  cnflf  22621  fclsopn  22633  fclsbas  22640  fclsrest  22643  isfcf  22653  cnfcf  22661  ptcmplem3  22673  tmdgsum2  22715  eltsms  22752  tsmsgsum  22758  tsmssubm  22762  tsmsf1o  22764  utopsnneiplem  22867  ismet2  22954  prdsxmetlem  22989  elmopn2  23066  prdsbl  23112  metss  23129  metrest  23145  metcnp  23162  metcnp2  23163  metcn  23164  metucn  23192  nrginvrcn  23312  metdsge  23468  divcn  23487  elcncf2  23509  mulc1cncf  23524  cncfmet  23528  evth2  23579  lmmbr2  23877  lmmbrf  23880  iscfil2  23884  cfil3i  23887  iscau2  23895  iscau4  23897  iscauf  23898  caucfil  23901  iscmet3lem3  23908  cfilres  23914  causs  23916  lmclim  23921  rrxmet  24026  evthicc2  24078  cniccbdd  24079  ovolfioo  24085  ovolficc  24086  ismbl2  24145  mbfsup  24282  mbfinf  24283  mbflimsup  24284  0plef  24290  mbfi1flim  24341  xrge0f  24349  itg2mulclem  24364  itgeqa  24431  ellimc2  24494  ellimc3  24496  limcflf  24498  cnlimc  24505  dvferm1  24602  dvferm2  24604  rolle  24607  dvivthlem1  24625  ftc1lem6  24658  itgsubst  24666  mdegle0  24692  deg1leb  24710  plydivex  24907  ulm2  24994  ulmcaulem  25003  ulmcau  25004  ulmdvlem3  25011  abelthlem9  25049  abelth  25050  rlimcnp  25565  ftalem3  25674  issqf  25735  sqf11  25738  dvdsmulf1o  25793  dchrelbas4  25841  dchrinv  25859  2sqlem6  26021  chpo1ubb  26079  dchrmusumlema  26091  dchrisum0lema  26112  ostth3  26236  tgcgr4  26339  eqeelen  26712  brbtwn2  26713  colinearalg  26718  axcgrid  26724  axsegconlem1  26725  ax5seglem4  26740  ax5seglem5  26741  axbtwnid  26747  axpasch  26749  axeuclidlem  26770  axcontlem2  26773  axcontlem4  26775  axcontlem7  26778  axcontlem12  26783  elntg2  26793  isuvtx  27199  uvtx2vtx1edg  27202  uvtx2vtx1edgb  27203  iscplgrnb  27220  iscplgredg  27221  vdiscusgrb  27334  uhgrvd00  27338  upgriswlk  27444  wwlksnext  27693  clwwlkinwwlk  27839  clwwlkel  27845  clwwlkf  27846  clwwlkwwlksb  27853  wwlksext2clwwlk  27856  wwlksubclwwlk  27857  clwwlknonex2lem2  27907  nmounbi  28573  blocnilem  28601  isph  28619  phoeqi  28654  h2hcau  28776  h2hlm  28777  hial2eq2  28904  hoeq1  29627  hoeq2  29628  adjsym  29630  cnvadj  29689  hhcno  29701  hhcnf  29702  adjvalval  29734  leop2  29921  leoptri  29933  mdbr2  30093  dmdbr2  30100  mddmd2  30106  cdj3lem3b  30237  infxrge0gelb  30530  toslublem  30694  tosglblem  30696  mgccnv  30721  submarchi  30884  isarchi3  30885  lindfpropd  31015  cmpcref  31239  lmdvg  31342  prodindf  31428  eulerpartlemd  31770  subfacp1lem3  32578  subfacp1lem5  32580  satfv1lem  32758  dfrdg2  33189  sltrec  33427  opnrebl  33817  poimirlem23  35120  broucube  35131  itg2gt0cn  35152  ftc1cnnc  35169  lmclim2  35236  caures  35238  sstotbnd2  35252  rrnmet  35307  rrncmslem  35310  isdrngo3  35437  isidlc  35493  cvrval2  36610  isat3  36643  iscvlat2N  36660  glbconN  36713  ltrneq  37485  cdlemefrs29clN  37735  cdlemefrs32fva  37736  cdleme32fva  37773  cdlemk33N  38245  cdlemk34  38246  cdlemkid3N  38269  cdlemkid4  38270  diaglbN  38391  dibglbN  38502  dihglbcpreN  38636  dihglblem6  38676  hdmap1eulem  39158  hdmap1eulemOLDN  39159  hdmapoc  39267  hlhilocv  39293  wepwsolem  40050  fnwe2lem2  40059  islnm2  40086  iscard5  40306  alephiso2  40321  clsk3nimkb  40807  ntrclsneine0  40832  ntrneineine0  40854  ntrneineine1  40855  ntrneicls00  40856  ntrneicls11  40857  ntrneiiso  40858  ntrneik2  40859  ntrneix2  40860  ntrneikb  40861  ntrneixb  40862  ntrneik3  40863  ntrneix3  40864  ntrneik13  40865  ntrneix13  40866  ntrneik4w  40867  ntrneik4  40868  caofcan  41091  infxrbnd2  42062  supminfxr  42164  evthiccabs  42194  ellimcabssub0  42320  climf  42325  clim2f  42339  clim2cf  42353  clim0cf  42357  limsupmnflem  42423  limsupre2lem  42427  limsupreuzmpt  42442  supcnvlimsup  42443  limsupge  42464  liminfreuzlem  42505  liminfltlem  42507  liminflimsupclim  42510  liminfpnfuz  42519  xlimpnfxnegmnf2  42561  fourierdlem70  42879  fourierdlem71  42880  fourierdlem73  42882  fourierdlem80  42889  fourierdlem83  42892  fourierdlem87  42896  voliunsge0lem  43172  meaiuninclem  43180  meaiuninc3v  43184  hoidmv1lelem3  43293  hoidmvlelem4  43298  hoidmvlelem5  43299  issmflem  43422  requad2  44202  islinindfis  44917  elbigolo1  45030  line2x  45227  itscnhlinecirc02p  45258  aacllem  45388
 Copyright terms: Public domain W3C validator