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

Theorem ralbidv 3174
Description: Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.)
Hypothesis
Ref Expression
ralbidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
ralbidv (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralbidv
StepHypRef Expression
1 ralbidv.1 . . 3 (𝜑 → (𝜓𝜒))
21adantr 468 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32ralbidva 3173 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wcel 2156  wral 3096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001
This theorem depends on definitions:  df-bi 198  df-an 385  df-ral 3101
This theorem is referenced by:  2ralbidv  3177  rexralbidv  3246  raleqbi1dv  3335  raleqbidv  3341  cbvral2v  3368  rspceaimv  3510  rspc2  3513  rspc3v  3518  reu6i  3595  reu7  3599  sbcralt  3706  reu8nf  3711  raaan  4275  2ralsng  4413  issn  4551  2ralunsn  4617  elintg  4677  elintrabg  4682  eliin  4717  disjprg  4840  disjxun  4842  brralrspcev  4904  reusv2lem2  5068  reusv3  5074  poeq1  5235  somo  5266  frirr  5288  fr2nr  5289  frminex  5291  wereu2  5308  posn  5389  frsn  5391  ralxpf  5470  cnvpo  5887  fnmptfvd  6542  iinpreima  6567  dff4  6595  dff13f  6737  fpropnf1  6748  eusvobj2  6867  ovanraleqv  6898  ofreq  7130  sorpssuni  7176  sorpssint  7177  fr3nr  7209  onssmin  7227  funcnvuni  7349  f1oweALT  7382  frxp  7521  wrecseq123  7643  wfrlem1  7649  wfrlem3a  7652  wfrlem15  7665  smoeq  7683  tfrlem12  7721  tz7.48lem  7772  elixp2  8149  undifixp  8181  xpf1o  8361  nneneq  8382  ac6sfi  8443  frfi  8444  fipreima  8511  indexfi  8513  marypha1lem  8578  marypha1  8579  supeq1  8590  supeq3  8594  supmo  8597  eqsup  8601  supub  8604  suplub  8605  sup0  8611  supisoex  8619  eqinf  8629  infval  8631  infmo  8640  oieq1  8656  ordtypecbv  8661  ordtypelem3  8664  ordtypelem6  8667  ordtypelem7  8668  ordtypelem9  8670  wemaplem1  8690  wemaplem2  8691  zfregcl  8738  oemapval  8827  oemapvali  8828  cantnf  8837  wemapwe  8841  rankval3b  8936  unbndrank  8952  rankunb  8960  rankuni2b  8963  tcrank  8994  scottex  8995  scottexs  8997  scott0s  8998  bnd2  9003  updjud  9043  dfac8clem  9138  ac5num  9142  acni  9151  acni2  9152  alephval3  9216  dfac4  9228  dfac5lem5  9233  dfac5  9234  dfac2a  9235  dfac2b  9236  dfac2OLD  9238  dfacacn  9248  kmlem2  9258  kmlem13  9269  cflem  9353  cflecard  9360  cfeq0  9363  cfsuc  9364  cfflb  9366  cofsmo  9376  cfsmolem  9377  cfcoflem  9379  coftr  9380  alephsing  9383  fin23lem11  9424  isfin3ds  9436  fin23lem17  9445  fin23lem39  9457  isf33lem  9473  isf34lem6  9487  fin1a2lem13  9519  hsmexlem4  9536  hsmex  9539  axcc2lem  9543  axcc3  9545  dcomex  9554  axdc2lem  9555  axdc3lem2  9558  axdc3lem3  9559  axdc3  9561  axdc4lem  9562  axcclem  9564  zorn2lem2  9604  zorn2lem7  9609  zorn2g  9610  zornn0g  9612  ttukeylem7  9622  axdclem2  9627  brdom3  9635  brdom7disj  9638  brdom6disj  9639  alephval2  9679  inar1  9882  axgroth6  9935  pinq  10034  nqereu  10036  prlem934  10140  supexpr  10161  supsrlem  10217  axpre-sup  10275  dedekind  10485  dedekindle  10486  fiminre  11257  lbreu  11258  sup2  11264  infm3  11267  nnsub  11345  uzwo  11970  nnwof  11973  ublbneg  11992  lbzbi  11995  zsupss  11996  uzsupss  11999  uzwo3  12002  zmax  12004  rpnnen1lem1  12034  rpnnen1lem3  12035  rpnnen1lem4  12036  rpnnen1lem5  12037  xrsupsslem  12355  xrinfmsslem  12356  xrsupss  12357  xrinfmss  12358  flval2  12839  axdc4uzlem  13006  ssnn0fi  13008  fsuppmapnn0fiubex  13015  faclbnd4lem4  13303  bccl  13329  hashgt12el  13427  hashbc  13454  hashge2el2dif  13479  wrdind  13700  wrd2ind  13701  rexanre  14309  rexico  14316  cau4  14319  clim  14448  rlim  14449  rlim2  14450  clim2  14458  clim2c  14459  clim0c  14461  rlim0  14462  rlim0lt  14463  ello12r  14471  ello1d  14477  elo12r  14482  rlimresb  14519  rlimcld2  14532  climabs0  14539  rlimo1  14570  lo1add  14580  lo1mul  14581  isercoll  14621  incexclem  14790  sqrt2irr  15199  gcdcllem1  15440  gcdcllem2  15441  dfgcd2  15482  fissn0dvds  15551  dvdslcmf  15563  lcmfledvds  15564  lcmf  15565  lcmfunsnlem1  15569  lcmfunsnlem2lem1  15570  lcmfunsnlem  15573  lcmfdvds  15574  reumodprminv  15726  pc2dvds  15800  pcz  15802  prmpwdvds  15825  infpn2  15834  prmreclem2  15838  prmreclem3  15839  prmreclem5  15841  prmreclem6  15842  vdwlem6  15907  vdwlem8  15909  vdwlem13  15914  vdwnnlem1  15916  vdwnn  15919  ramcl  15950  cshwrepswhash1  16021  prdsleval  16342  imasval  16376  imasaddfnlem  16393  imasvscafn  16402  mrisval  16495  isacs  16516  isacs2  16518  isacs1i  16522  mreacs  16523  acsfn  16524  acsfn2  16528  iscatd  16538  catidex  16539  catideu  16540  cidval  16542  catidd  16545  comfeq  16570  catpropd  16573  ismon  16597  isfunc  16728  isnat  16811  isinito  16854  istermo  16855  isprs  17135  drsdirfi  17143  ispos  17152  lubfval  17183  lubeldm  17186  lubval  17189  lubprop  17191  lublecllem  17193  glbfval  17196  glbeldm  17199  glbval  17202  glbprop  17204  joinval2lem  17213  joinlem  17216  meetval2lem  17227  meetlem  17230  isglbd  17322  lubl  17325  lubun  17328  clatleglb  17331  poslubmo  17351  posglbmo  17352  poslubd  17353  ipodrsima  17370  isdlat  17398  mgm1  17462  gsumval2  17485  sgrp1  17498  mhmima  17568  mrcmndind  17571  gsumwspan  17588  sgrp2rid2  17618  sgrp2rid2ex  17619  sgrp2nmndlem4  17620  dfgrp2  17652  isgrpinv  17677  grpidinv  17680  dfgrp3lem  17718  issubg4  17815  0subg  17821  cycsubgcl  17822  isnsg2  17826  nsgacs  17832  elnmz  17835  ghmrn  17875  ghmnsgima  17886  isga  17925  orbsta  17947  cntzfval  17954  elcntz  17956  resscntz  17965  oppgsubg  17994  symgextfo  18043  gsmsymgreqlem2  18052  gsmsymgreq  18053  pmtrdifel  18101  pmtrdifwrdellem3  18104  pmtrdifwrdel2  18107  psgnunilem2  18116  psgnunilem3  18117  odeq  18170  gexid  18197  gexlem2  18198  gexdvds  18200  isslw  18224  sylow2alem1  18233  sylow2alem2  18234  efgval  18331  efgrelexlemb  18364  efgcpbllemb  18369  abl1  18470  dmdprd  18599  dprd2da  18643  pgpfac1lem5  18680  ring1  18804  isabv  19023  islss  19139  lssacs  19174  reslmhm  19259  islbs  19283  pj1lmhm  19307  lbsacsbs  19365  isrrg  19497  opsrval  19683  ply1coe  19874  cply1coe0bi  19878  zringlpir  20045  psgndiflemA  20155  ocvfval  20220  elocv  20222  iunocv  20235  frlmlbs  20346  islindf  20361  islinds2  20362  islindf2  20363  lindfrn  20370  lsslindf  20379  islindf4  20387  mat0dimcrng  20487  mdetunilem1  20629  mdetunilem9  20637  cpmat  20727  cpmatel  20729  1elcpmat  20733  m2cpminvid2lem  20772  basgen2  21007  bastop1  21011  isclo  21105  ordtbaslem  21206  iscn  21253  cnpval  21254  iscnp  21255  iscnp3  21262  lmbr  21276  lmbr2  21277  lmbrf  21278  cnprest  21307  cnprest2  21308  t0sep  21342  isreg  21350  t1sep2  21387  tgcmp  21418  1stcclb  21461  1stcfb  21462  2ndc1stc  21468  1stcrest  21470  2ndcdisj  21473  islly  21485  isnlly  21486  lly1stc  21513  isref  21526  islocfin  21534  elkgen  21553  kgencn  21573  elpt  21589  elptr  21590  ptcnplem  21638  tx1stc  21667  cnmpt21  21688  kqt0lem  21753  isr0  21754  regr1lem2  21757  r0sep  21765  nrmr0reg  21766  flffbas  22012  cnflf  22019  cnflf2  22020  lmflf  22022  txflf  22023  fclsopni  22032  fclsnei  22036  fclsrest  22041  fcfnei  22052  cnfcf  22059  alexsubb  22063  alexsubALTlem3  22066  qustgplem  22137  tsmsfbas  22144  tsmsres  22160  tsmsf1o  22161  tsmsxplem1  22169  ustval  22219  isust  22220  ustincl  22224  ustdiag  22225  ustinvel  22226  ustexhalf  22227  ust0  22236  utopval  22249  ucnval  22294  isucn  22295  isucn2  22296  ucnima  22298  iscfilu  22305  ispsmet  22322  ismet  22341  isxmet  22342  imasdsf1olem  22391  imasf1oxmet  22393  imasf1omet  22394  metss  22526  met1stc  22539  prdsxmslem2  22547  txmetcnp  22565  metucn  22589  tngngp3  22673  nlmvscn  22704  nmoval  22732  nmolb  22734  qtopbaslem  22775  cncfval  22904  elcncf2  22906  mulc1cncf  22921  cncfmet  22924  evth  22971  lebnumlem3  22975  lebnum  22976  xlebnum  22977  ishtpy  22984  isphtpy  22993  pi1xfr  23067  pi1coghm  23073  isclmp  23109  ipcn  23257  lmmbr2  23269  lmmbr3  23270  lmmbrf  23272  cfilfval  23274  iscfil  23275  fmcfil  23282  caufval  23285  iscau  23286  iscau2  23287  iscau3  23288  iscau4  23289  iscauf  23290  caucfil  23293  cfilresi  23305  causs  23308  lmclim  23313  cmetcusp1  23361  minveclem4c  23408  minveclem2  23409  minveclem3b  23411  minveclem4  23415  minveclem6  23417  minveclem7  23418  ovolicc2lem3  23500  ismbl  23507  dyadmax  23579  dyadmbllem  23580  dyadmbl  23581  opnmbllem  23582  ismbf1  23605  ismbf  23609  mbfeqalem2  23623  mbflimsup  23647  mbfi1fseqlem6  23701  mbfi1flimlem  23703  itg2seq  23723  itg2monolem1  23731  isibl  23746  ply1divex  24110  fta1g  24141  dgrco  24245  plydivex  24266  fta1  24277  vieta1  24281  aannenlem1  24297  aannenlem2  24298  aalioulem2  24302  aalioulem3  24303  ulmval  24348  ulm2  24353  ulmi  24354  ulmres  24356  ulmshftlem  24357  ulmcaulem  24362  ulmcau  24363  ulmss  24365  ulmbdd  24366  ulmdvlem1  24368  ulmdvlem3  24370  pilem2  24420  pilem3  24421  pilem3OLD  24422  cxpcn3  24703  dmarea  24898  rlimcnp  24906  scvxcvx  24926  lgamgulmlem2  24970  lgamgulmlem3  24971  lgamgulmlem5  24973  lgambdd  24977  lgamcvglem  24980  isppw2  25055  perfectlem2  25169  2sqlem6  25362  2sqlem10  25367  dchrisumlema  25391  dchrisumlem2  25393  dchrisumlem3  25394  pntpbnd  25491  pntibndlem3  25495  pntibnd  25496  pntleme  25511  pntlem3  25512  pntlemp  25513  pnt3  25515  istrkgld  25572  axtg5seg  25578  tgcgr4  25640  perpln1  25819  perpln2  25820  isperp  25821  brbtwn2  25999  colinearalg  26004  axsegconlem1  26011  axsegcon  26021  ax5seglem4  26026  ax5seglem5  26027  axlowdim  26055  axeuclidlem  26056  axcontlem1  26058  axcontlem2  26059  axcontlem4  26061  axcontlem5  26062  axcontlem8  26065  axcontlem12  26069  uvtxa01vtx0OLD  26520  uvtxusgr  26525  iscusgredg  26547  rgrx0ndm  26717  ewlksfval  26725  wksfval  26733  wwlks  26956  wlkiswwlks2  27002  clwwlk  27126  1conngr  27367  frgrwopregasn  27491  frgrwopregbsn  27492  frgrwopreglem5ALT  27497  frgrregord013  27583  isgrpo  27680  isgrpoi  27681  grpoideu  27692  grpoidinv2  27698  vciOLD  27744  isvclem  27760  cnidOLD  27765  isnvlem  27793  nvi  27797  lnoval  27935  islno  27936  isblo3i  27984  blo3i  27985  blocnilem  27987  ajfval  27992  ubthlem1  28054  ubthlem2  28055  ubthlem3  28056  ubth  28057  minvecolem2  28059  minvecolem3  28060  minvecolem4c  28063  minvecolem4  28064  minvecolem5  28065  minvecolem6  28066  minvecolem7  28067  h2hcau  28164  h2hlm  28165  hilid  28346  hcau  28369  hlimi  28373  hlim2  28377  ocel  28468  adjsym  29020  ellnop  29045  ellnfn  29070  hhcno  29091  hhcnf  29092  lnopeq  29196  elunop2  29200  lnophm  29206  lnconi  29220  lnopcnbd  29223  lnfncnbd  29244  imaelshi  29245  riesz3i  29249  riesz4i  29250  riesz4  29251  riesz1  29252  cnlnadjlem2  29255  cnlnadjlem5  29258  cnlnadjlem8  29261  cnlnadji  29263  nmopadjlei  29275  cnvbraval  29297  leopg  29309  leoppos  29313  mdbr  29481  dmdbr  29486  cdj3i  29628  disjunsn  29732  funcnv5mpt  29796  fgreu  29798  fcnvgreu  29799  xrge0infss  29852  resspos  29984  isomnd  30026  inftmrel  30059  isinftm  30060  archiabl  30077  isarchiofld  30142  crefeq  30237  esum2d  30480  sigaval  30498  issgon  30511  isrnmeas  30588  ismbfm  30639  isanmbfm  30643  mbfmcst  30646  elcarsg  30692  sitgval  30719  eulerpartlemd  30753  ballotleme  30883  tgoldbachgt  31066  bnj1185  31187  bnj1385  31226  bnj66  31253  bnj106  31261  bnj155  31272  bnj852  31314  bnj893  31321  bnj1228  31402  bnj1234  31404  bnj1463  31446  derangenlem  31476  subfacp1lem3  31487  subfacp1lem5  31489  subfacp1lem6  31490  subfacp1  31491  erdszelem8  31503  kur14  31521  cnpconn  31535  resconn  31551  cvmscbv  31563  iscvm  31564  cvmsi  31570  cvmsval  31571  cvmlift3lem2  31625  snmlval  31636  mclsssvlem  31782  mclsval  31783  mclsax  31789  mclsind  31790  dfpo2  31967  dfon2lem9  32016  dfrdg2  32021  dfrdg3  32022  frpomin  32059  poseq  32074  soseq  32075  frecseq123  32098  frrlem1  32101  sltval  32121  noprefixmo  32169  nosupno  32170  nosupdm  32171  nosupfv  32173  nosupres  32174  nosupbnd1lem1  32175  nosupbnd1lem3  32177  nosupbnd1lem5  32179  noetalem5  32188  noeta  32189  nocvxminlem  32214  brsslt  32221  conway  32231  etasslt  32241  slerec  32244  fwddifnval  32591  nn0prpwlem  32638  isfne  32655  isfne4  32656  isfne2  32658  isfne3  32659  neibastop3  32678  topmeet  32680  topjoin  32681  filnetlem4  32697  unblimceq0lem  32814  unblimceq0  32815  unbdqndv2  32819  taupilemrplb  33483  csbwrecsg  33490  fin2so  33709  matunitlindflem2  33719  ptrecube  33722  poimirlem2  33724  poimirlem3  33725  poimirlem4  33726  poimirlem24  33746  poimirlem25  33747  poimirlem26  33748  poimirlem27  33749  poimirlem28  33750  poimirlem29  33751  poimirlem30  33752  poimirlem32  33754  poimir  33755  heicant  33757  mblfinlem1  33759  mblfinlem2  33760  voliunnfl  33766  volsupnfl  33767  mbfresfi  33768  itg2addnc  33776  f1opr  33831  upixp  33836  indexdom  33841  filbcmb  33847  sdclem2  33849  fdc  33852  lmclim2  33865  caures  33867  istotbnd  33879  istotbnd3  33881  sstotbnd  33885  isbnd  33890  heibor  33931  bfp  33934  rrncmslem  33942  isgrpda  34065  idlval  34123  isidl  34124  0idl  34135  unichnidl  34141  pridl  34147  ismaxidl  34150  smprngopr  34162  igenval2  34176  prnc  34177  ispridlc  34180  scottexf  34286  scott0f  34287  riotasvd  34735  islfl  34840  eqlkr  34879  eqlkr3  34881  glbconN  35157  hlsuprexch  35161  ispsubsp  35525  ldilset  35889  isldil  35890  dilsetN  35934  isdilN  35935  trlset  35942  trlval  35943  cdleme27b  36149  cdleme29b  36156  cdleme31so  36160  cdleme31sn1  36162  cdleme31sn1c  36169  cdleme31fv  36171  cdleme40v  36250  istendo  36541  cdlemkid3N  36714  cdlemkid4  36715  cdlemkid5  36716  dihfval  37012  dihval  37013  islpolN  37264  hdmapffval  37607  hdmapfval  37608  hdmapval  37609  hdmapval2lem  37612  hgmapffval  37666  hgmapfval  37667  hgmapval  37668  hgmapvs  37672  isnacs  37769  isnacs2  37771  nacsfix  37777  mzpclval  37790  elmzpcl  37791  rencldnfilem  37886  infmrgelbi  37944  pellfundre  37947  pellfundlb  37950  wepwsolem  38113  fnwe2lem2  38122  aomclem8  38132  dfac11  38133  gicabl  38170  islnr3  38186  hbtlem2  38195  hbtlem5  38199  fiinfi  38378  clsk1independent  38844  ntrclsk13  38869  gneispacess2  38944  imo72b2lem0  38965  imo72b2lem2  38967  imo72b2lem1  38971  imo72b2  38975  evth2f  39668  evthf  39680  fnchoice  39682  uzwo4  39714  wessf1ornlem  39860  disjinfi  39869  rnmptlb  39937  rnmptbdd  39940  rnmptbd2  39947  rnmptbd  39954  dstregt0  39975  upbdrech2  40003  fiminre2  40074  rexabslelem  40124  rexabsle  40125  uzub  40137  infrpgernmpt  40174  mccl  40310  ellimcabssub0  40329  climf  40334  clim2f  40348  limsupre  40353  clim2cf  40362  clim0cf  40366  climf2  40378  clim2f2  40382  clim2d  40385  limsupref  40397  limsupbnd1f  40398  limsuppnfd  40414  climinf2  40419  limsuppnf  40423  climinfmpt  40427  climinf3  40428  limsupubuzmpt  40431  limsupmnf  40433  limsupre2lem  40436  limsupre2  40437  limsupmnfuzlem  40438  limsupmnfuz  40439  limsupre2mpt  40442  limsupre3lem  40444  limsupre3  40445  limsupre3mpt  40446  limsupre3uz  40448  limsupreuz  40449  limsupreuzmpt  40451  climuz  40456  liminfreuzlem  40514  liminfreuz  40515  cnrefiisplem  40535  xlimmnfvlem1  40538  xlimmnfv  40540  xlimpnfvlem1  40542  xlimpnfv  40544  xlimmnfmpt  40549  xlimpnfmpt  40550  cncfshift  40567  cncfperiod  40572  fperdvper  40613  dvbdfbdioo  40625  ioodvbdlimc1lem2  40627  ioodvbdlimc2lem  40629  dvnprodlem3  40643  stoweidlem5  40701  stoweidlem9  40705  stoweidlem15  40711  stoweidlem16  40712  stoweidlem27  40723  stoweidlem28  40724  stoweidlem31  40727  stoweidlem34  40730  stoweidlem37  40733  stoweidlem46  40742  stoweidlem48  40744  stoweidlem51  40747  stoweidlem52  40748  stoweidlem59  40755  wallispilem3  40763  stirlinglem13  40782  fourierdlem2  40805  fourierdlem3  40806  fourierdlem16  40819  fourierdlem20  40823  fourierdlem21  40824  fourierdlem22  40825  fourierdlem25  40828  fourierdlem39  40842  fourierdlem42  40845  fourierdlem54  40856  fourierdlem64  40866  fourierdlem77  40879  fourierdlem83  40885  fourierdlem103  40905  fourierdlem104  40906  subsaliuncllem  41054  ismea  41147  iundjiun  41156  meaiunincf  41179  caragenval  41189  isome  41190  caragenel  41191  omessle  41194  ovnlerp  41258  hoidmvlelem3  41293  hoidmvle  41296  issmflem  41418  issmfgt  41447  smfmullem2  41481  smfmullem4  41483  smfmul  41484  smfsuplem2  41500  smfsup  41502  smfinflem  41505  smfinf  41506  raaan2  41649  cbvral2  41685  2reu4a  41701  dfdfat2  41717  iccpart  41927  iccpartigtl  41934  perfectALTVlem2  42206  bgoldbachlt  42276  tgoldbachlt  42279  upwlksfval  42284  mgmhmima  42370  rnghmval  42459  lidlmsgrp  42494  lidlrng  42495  uzlidlring  42497  ply1mulgsumlem1  42742  ply1mulgsumlem2  42743  linindslinci  42805  lindslinindsimp1  42814  lindslinindsimp2lem5  42819  lindslinindsimp2  42820  linds0  42822  lindsrng01  42825  snlindsntor  42828  lmod1  42849  ldepsnlinc  42865  bigoval  42911  elbigo2r  42915  nn0sumshdiglem2  42984  setrec1lem2  43003
  Copyright terms: Public domain W3C validator