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

Theorem ralbidva 3014
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 723 . 2 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
32ralbidv2 3013 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wcel 2030  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-an 385  df-ral 2946
This theorem is referenced by:  ralbidv  3015  2ralbidva  3017  raleqbidva  3184  poinxp  5216  soinxp  5217  frinxp  5218  ordunisssuc  5868  fnmptfvd  6360  funimass3  6373  fnnfpeq0  6485  cocan1  6586  cocan2  6587  isores2  6623  isoini2  6629  ofrfval  6947  ofrfval2  6957  tfindsg2  7103  f1oweALT  7194  fnsuppres  7367  dfsmo2  7489  smores  7494  smores2  7496  dfrecs3  7514  ac6sfi  8245  fimaxg  8248  ordunifi  8251  isfinite2  8259  fipreima  8313  supisolem  8420  fiming  8445  infempty  8453  ordiso2  8461  ordtypelem7  8470  cantnf  8628  wemapwe  8632  rankval3b  8727  rankonidlem  8729  iscard  8839  acndom  8912  dfac12lem3  9005  kmlem2  9011  cflim2  9123  cfsmolem  9130  ttukeylem6  9374  alephreg  9442  suplem2pr  9913  axsup  10151  sup3  11018  infm3  11020  suprleub  11027  dfinfre  11042  infregelb  11045  ofsubeq0  11055  ofsubge0  11057  zextlt  11489  prime  11496  suprfinzcl  11530  indstr  11794  supxr2  12182  supxrbnd1  12189  supxrbnd2  12190  supxrleub  12194  supxrbnd  12196  infxrgelb  12203  fzshftral  12466  mptnn0fsupp  12837  swrdeq  13490  swrdspsleq  13495  clim  14269  rlim  14270  clim2  14279  clim2c  14280  clim0c  14282  ello1mpt  14296  lo1o1  14307  o1lo1  14312  climabs0  14360  o1compt  14362  rlimdiv  14420  geomulcvg  14651  mertenslem2  14661  mertens  14662  rpnnen2lem12  14998  sqrt2irr  15023  fprodfvdvdsd  15105  fproddvdsd  15106  dfgcd2  15310  isprm7  15467  pc11  15631  pcz  15632  1arith  15678  vdwlem8  15739  vdwlem11  15742  vdw  15745  ramval  15759  pwsle  16199  mrieqvd  16345  mreacs  16366  cidpropd  16417  ismon2  16441  monpropd  16444  isepi  16447  isepi2  16448  subsubc  16560  funcres2b  16604  funcpropd  16607  isfull2  16618  isfth2  16622  fucsect  16679  fucinv  16680  pospropd  17181  ipodrsfi  17210  tsrss  17270  grpidpropd  17308  mndpropd  17363  grppropd  17484  issubg4  17660  gass  17780  gsmsymgrfixlem1  17893  gsmsymgreqlem2  17897  gexdvds  18045  gexdvds2  18046  subgpgp  18058  sylow3lem6  18093  efgval2  18183  efgsp1  18196  dprdf11  18468  subgdmdprd  18479  ringpropd  18628  abvpropd  18890  lsspropd  19065  lbspropd  19147  assapropd  19375  psrbaglefi  19420  psrbagconf1o  19422  gsumbagdiaglem  19423  mplmonmul  19512  gsumply1eq  19723  phlpropd  20048  ishil2  20111  lindfmm  20214  islindf4  20225  islindf5  20226  scmatf1  20385  cpmatmcllem  20571  cpmatmcl  20572  decpmataa0  20621  decpmatmulsumfsupp  20626  pmatcollpw2lem  20630  pm2mpmhmlem1  20671  tgss2  20839  isclo  20939  neips  20965  opnnei  20972  isperf3  21005  ssidcn  21107  lmbrf  21112  cnnei  21134  cnrest2  21138  lmss  21150  lmres  21152  ist1-2  21199  ist1-3  21201  isreg2  21229  cmpfi  21259  bwth  21261  1stccn  21314  subislly  21332  kgencn  21407  ptclsg  21466  ptcnplem  21472  xkococnlem  21510  xkoinjcn  21538  tgqtop  21563  qtopcn  21565  fbflim  21827  flimrest  21834  flfnei  21842  isflf  21844  cnflf  21853  fclsopn  21865  fclsbas  21872  fclsrest  21875  isfcf  21885  cnfcf  21893  ptcmplem3  21905  tmdgsum2  21947  eltsms  21983  tsmsgsum  21989  tsmssubm  21993  tsmsf1o  21995  utopsnneiplem  22098  ismet2  22185  prdsxmetlem  22220  elmopn2  22297  prdsbl  22343  metss  22360  metrest  22376  metcnp  22393  metcnp2  22394  metcn  22395  metucn  22423  nrginvrcn  22543  metdsge  22699  divcn  22718  elcncf2  22740  mulc1cncf  22755  cncfmet  22758  evth2  22806  lmmbr2  23103  lmmbrf  23106  iscfil2  23110  cfil3i  23113  iscau2  23121  iscau4  23123  iscauf  23124  caucfil  23127  iscmet3lem3  23134  cfilres  23140  causs  23142  lmclim  23147  rrxmet  23237  evthicc2  23275  cniccbdd  23276  ovolfioo  23282  ovolficc  23283  ismbl2  23341  mbfsup  23476  mbfinf  23477  mbflimsup  23478  0plef  23484  mbfi1flim  23535  xrge0f  23543  itg2mulclem  23558  itgeqa  23625  ellimc2  23686  ellimc3  23688  limcflf  23690  cnlimc  23697  dvferm1  23793  dvferm2  23795  rolle  23798  dvivthlem1  23816  ftc1lem6  23849  itgsubst  23857  mdegle0  23882  deg1leb  23900  plydivex  24097  ulm2  24184  ulmcaulem  24193  ulmcau  24194  ulmdvlem3  24201  abelthlem9  24239  abelth  24240  rlimcnp  24737  ftalem3  24846  issqf  24907  sqf11  24910  dvdsmulf1o  24965  dchrelbas4  25013  dchrinv  25031  2sqlem6  25193  chpo1ubb  25215  dchrmusumlema  25227  dchrisum0lema  25248  ostth3  25372  tgcgr4  25471  eqeelen  25829  brbtwn2  25830  colinearalg  25835  axcgrid  25841  axsegconlem1  25842  ax5seglem4  25857  ax5seglem5  25858  axbtwnid  25864  axpasch  25866  axeuclidlem  25887  axcontlem2  25890  axcontlem4  25892  axcontlem7  25895  axcontlem12  25900  isuvtx  26343  isuvtxaOLD  26344  uvtx2vtx1edg  26349  uvtx2vtx1edgb  26350  iscplgrnb  26368  iscplgredg  26369  vdiscusgrb  26482  uhgrvd00  26486  upgriswlk  26593  wwlksnext  26856  clwwlkinwwlk  27003  clwwlkel  27009  clwwlkf  27010  clwwlkwwlksb  27018  wwlksext2clwwlk  27021  wwlksext2clwwlkOLD  27022  wwlksubclwwlk  27023  clwlksfclwwlk  27049  clwwlknonex2lem2  27083  nmounbi  27759  blocnilem  27787  isph  27805  phoeqi  27841  h2hcau  27964  h2hlm  27965  hial2eq2  28092  hoeq1  28817  hoeq2  28818  adjsym  28820  cnvadj  28879  hhcno  28891  hhcnf  28892  adjvalval  28924  leop2  29111  leoptri  29123  mdbr2  29283  dmdbr2  29290  mddmd2  29296  cdj3lem3b  29427  infxrge0gelb  29659  toslublem  29795  tosglblem  29797  submarchi  29868  isarchi3  29869  cmpcref  30045  lmdvg  30127  prodindf  30213  eulerpartlemd  30556  subfacp1lem3  31290  subfacp1lem5  31292  dfrdg2  31825  sltrec  32049  opnrebl  32440  poimirlem23  33562  broucube  33573  itg2gt0cn  33595  ftc1cnnc  33614  lmclim2  33684  caures  33686  sstotbnd2  33703  rrnmet  33758  rrncmslem  33761  isdrngo3  33888  isidlc  33944  cvrval2  34879  isat3  34912  iscvlat2N  34929  glbconN  34981  ltrneq  35753  cdlemefrs29clN  36004  cdlemefrs32fva  36005  cdleme32fva  36042  cdlemk33N  36514  cdlemk34  36515  cdlemkid3N  36538  cdlemkid4  36539  diaglbN  36661  dibglbN  36772  dihglbcpreN  36906  dihglblem6  36946  hdmap1eulem  37430  hdmap1eulemOLDN  37431  hdmapoc  37540  hlhilocv  37566  wepwsolem  37929  fnwe2lem2  37938  islnm2  37965  clsk3nimkb  38655  ntrclsneine0  38680  ntrneineine0  38702  ntrneineine1  38703  ntrneicls00  38704  ntrneicls11  38705  ntrneiiso  38706  ntrneik2  38707  ntrneix2  38708  ntrneikb  38709  ntrneixb  38710  ntrneik3  38711  ntrneix3  38712  ntrneik13  38713  ntrneix13  38714  ntrneik4w  38715  ntrneik4  38716  caofcan  38839  infxrbnd2  39898  supminfxr  40007  evthiccabs  40036  ellimcabssub0  40167  climf  40172  clim2f  40186  clim2cf  40200  clim0cf  40204  limsupmnflem  40270  limsupre2lem  40274  limsupreuzmpt  40289  supcnvlimsup  40290  limsupge  40311  liminfreuzlem  40352  liminfltlem  40354  liminflimsupclim  40357  fourierdlem70  40711  fourierdlem71  40712  fourierdlem73  40714  fourierdlem80  40721  fourierdlem83  40724  fourierdlem87  40728  voliunsge0lem  41007  meaiuninclem  41015  meaiuninc3v  41019  hoidmv1lelem3  41128  hoidmvlelem4  41133  hoidmvlelem5  41134  issmflem  41257  pfxeq  41729  islinindfis  42563  elbigolo1  42676  aacllem  42875
  Copyright terms: Public domain W3C validator