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

Theorem ralbii 3009
 Description: Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 4-Dec-2019.)
Hypothesis
Ref Expression
ralbii.1 (𝜑𝜓)
Assertion
Ref Expression
ralbii (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓)

Proof of Theorem ralbii
StepHypRef Expression
1 ralbii.1 . . 3 (𝜑𝜓)
21imbi2i 325 . 2 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32ralbii2 3007 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∈ 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 This theorem depends on definitions:  df-bi 197  df-ral 2946 This theorem is referenced by:  2ralbii  3010  dfral2  3023  ralinexa  3026  rexanali  3027  nrexralim  3028  r19.23v  3052  r19.26-2  3094  r19.26-3  3095  ralbiim  3098  r19.28v  3100  r19.30  3111  r19.32v  3112  r19.35  3113  ralcom13  3129  ralrot3  3131  cbvral2v  3209  cbvral3v  3211  sbralie  3214  ralcom4  3255  ralxpxfr2d  3358  reu8  3435  2reuswap  3443  2reu5lem2  3447  dfss5  3897  n0el  3973  ralnralall  4113  r19.12sn  4287  ssdifsn  4351  raldifsnb  4358  eqsn  4393  eqsnOLD  4394  n0snor2el  4396  uni0b  4495  uni0c  4496  ssint  4525  iuniin  4563  iuneq2  4569  iunss  4593  ssiinf  4601  iinab  4613  iinun2  4618  iindif2  4621  iinin2  4622  iinuni  4641  sspwuni  4643  iinpw  4649  disjor  4666  disjxun  4683  dftr3  4789  trint  4801  reusv3  4906  reuxfr2d  4921  otiunsndisj  5009  ssrel2  5244  reliun  5272  xpiindi  5290  rexiunxp  5295  ralxpf  5301  rexxpf  5302  dfse2  5534  asymref2  5548  rninxp  5608  dminxp  5609  cnviin  5710  cnvpo  5711  wfis2fg  5755  dffun9  5955  funcnv3  5997  fncnv  6000  fnres  6045  mptfnf  6053  fnopabg  6055  mptfng  6057  fint  6122  funimass4  6286  fndmdifeq0  6363  funconstss  6375  f1ompt  6422  fconstfv  6517  idref  6539  dff13f  6553  dff14b  6568  weniso  6644  foov  6850  dfwe2  7023  tfis2f  7097  tfindes  7104  frxp  7332  tz7.48lem  7581  tz7.49  7585  oeordi  7712  ixpeq2  7964  ixpin  7975  ixpiin  7976  boxriin  7992  findcard3  8244  fimax2g  8247  fissuni  8312  indexfi  8315  dfsup2  8391  sup0riota  8412  infcllem  8434  wemapsolem  8496  zfinf2  8577  oemapso  8617  zfregs2  8647  r1elss  8707  rankc1  8771  cp  8792  bnd2  8794  aceq1  8978  aceq2  8980  kmlem7  9016  kmlem12  9021  kmlem13  9022  kmlem15  9024  fin12  9273  ac6num  9339  ac6s2  9346  ac6sf  9349  ac6s4  9350  zorn2lem4  9359  zorn2lem6  9361  zorn2lem7  9362  zorng  9364  ttukeylem6  9374  brdom7disj  9391  brdom6disj  9392  fpwwe2  9503  fpwwe  9506  axgroth5  9684  axgroth4  9692  grothprim  9694  nqereu  9789  genpnnp  9865  dfinfre  11042  infrenegsup  11044  xrsupsslem  12175  xrinfmsslem  12176  xrinfmss2  12179  fzshftral  12466  fsuppmapnn0ub  12835  mptnn0fsuppr  12839  hashgt12el  13248  hashgt12el2  13249  hashbc  13275  s3iunsndisj  13753  cotr2g  13761  rexfiuz  14131  clim0  14281  rpnnen2lem12  14998  gcdcllem1  15268  absproddvds  15377  coprmproddvdslem  15423  vdwmc2  15730  vdwlem13  15744  vdwnn  15749  xpscf  16273  mreacs  16366  acsfn  16367  acsfn1  16369  acsfn2  16371  ispos2  16995  lublecllem  17035  oduglb  17186  odulub  17188  posglbd  17197  isnmnd  17345  gsumwspan  17430  isnsg2  17671  oppgid  17832  oppgcntz  17840  efgval2  18183  iscyggen2  18329  iscyg3  18334  oppr1  18680  isnirred  18746  lssne0  18999  isdomn2  19347  iunocv  20073  islindf4  20225  pmatcollpw2lem  20630  isbasis2g  20800  basdif0  20805  tgval2  20808  ntreq0  20929  isclo2  20940  opnnei  20972  neiptopnei  20984  lmres  21152  ist1-3  21201  cmpcov2  21241  cmpsub  21251  is1stc2  21293  1stccn  21314  kgencn  21407  eltx  21419  txkgen  21503  fbun  21691  trfbas  21695  fbunfip  21720  trfil2  21738  isufil2  21759  fixufil  21773  hausflim  21832  txflf  21857  fclsopn  21865  alexsubALTlem3  21900  isclmp  22943  iscau3  23122  iscau4  23123  caucfil  23127  bcth3  23174  ovolgelb  23294  dyadmax  23412  itg2leub  23546  itg2cn  23575  plydivex  24097  vieta1  24112  lgseisenlem2  25146  pnt3  25346  tglowdim2ln  25591  axcontlem12  25900  numedglnl  26084  vtxd0nedgb  26440  wlkvtxedg  26596  pthd  26721  2pthdlem1  26895  clwlkclwwlk  26968  clwlksfclwwlk  27049  3pthdlem1  27142  frgrregord013  27382  grpoidinvlem3  27488  nmoubi  27755  lnon0  27781  adjsym  28820  nmopub  28895  nmfnleub  28912  cvbr2  29270  chpssati  29350  chrelat2i  29352  chrelat3  29358  mdsymlem8  29397  ralcom4f  29444  moel  29451  uniinn0  29492  ssiun3  29502  disjnf  29510  disjorf  29518  disjunsn  29533  ac6sf2  29557  nn0min  29695  tosglblem  29797  archiabl  29880  eulerpartlems  30550  eulerpartlemr  30564  eulerpartlemn  30571  ballotlem7  30725  bnj110  31054  bnj92  31058  bnj539  31087  bnj540  31088  bnj580  31109  bnj978  31145  bnj1047  31167  bnj1128  31184  bnj1417  31235  bnj1421  31236  bnj1312  31252  bnj1498  31255  subfacp1lem3  31290  cvmlift2lem1  31410  cvmlift2lem12  31422  untuni  31712  dfso3  31727  dfpo2  31771  elintfv  31788  setinds  31807  setinds2f  31808  elpotr  31810  dfon2lem7  31818  dfon2lem9  31820  frins2fg  31872  soseq  31879  nosepon  31943  nomaxmo  31972  nosupbnd1lem4  31982  conway  32035  ssltun2  32041  etasslt  32045  slerec  32048  dfint3  32184  brlb  32187  gtinfOLD  32439  filnetlem4  32501  phpreu  33523  ptrecube  33539  poimirlem1  33540  poimirlem25  33564  poimirlem26  33565  poimirlem27  33566  poimirlem30  33569  mblfinlem2  33577  ftc1anc  33623  inixp  33653  ac6gf  33657  heibor1lem  33738  heiborlem1  33740  iscrngo2  33926  ac6s3f  34109  3ralbii  34155  idinxpssinxp2  34230  n0elqs  34239  ineleq  34259  refrelcosslem  34352  refrelcoss3  34353  lpssat  34618  lssat  34621  lcvbr2  34627  lcvbr3  34628  lfl1  34675  lub0N  34794  glb0N  34798  atlrelat1  34926  hlrelat2  35007  ispsubsp2  35350  pclclN  35495  cdleme25cv  35963  tendoeq2  36379  cdlemk35  36517  setindtrs  37909  cllem0  38188  ss2iundf  38268  ntrneixb  38710  gneispace  38749  undisjrab  38822  zfregs2VD  39390  iunssf  39577  disjinfi  39694  iuneqfzuz  39864  mccl  40148  limsupub  40254  limsuppnflem  40260  limsupre2lem  40274  lmbr3v  40295  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvnprodlem3  40481  fourierdlem103  40744  fourierdlem104  40745  sge0iunmpt  40953  meaiuninc3v  41019  hoidmvle  41135  issmff  41264  r19.32  41488  2rexrsb  41492  cbvral2  41493  2ralbiim  41495  rmoanim  41500  2rmoswap  41505  2reu3  41509  2reu4a  41510  otiunsndisjX  41621  copisnmnd  42134  lindslinindsimp1  42571  lindslinindsimp2  42577  snlindsntor  42585  ldepslinc  42623  setrec1lem3  42761  aacllem  42875
 Copyright terms: Public domain W3C validator