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

Theorem ralbii 2823
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  |-  ( ph  <->  ps )
Assertion
Ref Expression
ralbii  |-  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )

Proof of Theorem ralbii
StepHypRef Expression
1 ralbii.1 . . 3  |-  ( ph  <->  ps )
21imbi2i 319 . 2  |-  ( ( x  e.  A  ->  ph )  <->  ( x  e.  A  ->  ps )
)
32ralbii2 2821 1  |-  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    e. wcel 1904   A.wral 2756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690
This theorem depends on definitions:  df-bi 190  df-ral 2761
This theorem is referenced by:  2ralbii  2824  dfral2  2835  ralinexa  2838  rexanali  2839  nrexralim  2840  r19.23v  2863  r2exlem  2899  r19.26-2  2905  r19.26-3  2906  ralbiim  2909  r19.28v  2911  r19.30  2921  r19.32v  2922  r19.35  2923  cbvral2v  3013  cbvral3v  3015  sbralie  3018  ralcom4  3052  ralxpxfr2d  3152  reu8  3222  2reuswap  3230  2reu5lem2  3234  r19.12sn  4029  raldifsnb  4094  eqsn  4125  uni0b  4215  uni0c  4216  ssint  4242  iuniin  4280  iuneq2  4286  iunss  4310  ssiinf  4318  iinab  4330  iinun2  4335  iindif2  4338  iinin2  4339  iinuni  4358  sspwuni  4360  iinpw  4363  disjor  4380  disjxun  4393  dftr3  4494  trint  4505  reusv3  4609  reuxfr2d  4623  otiunsndisj  4707  ssrel2  4930  reliun  4959  xpiindi  4975  rexiunxp  4980  ralxpf  4986  rexxpf  4987  dfse2  5208  asymref2  5223  rninxp  5282  dminxp  5283  cnviin  5380  cnvpo  5381  wfis2fg  5424  dffun9  5617  funcnv3  5654  fncnv  5657  fnres  5702  mptfnf  5709  fnopabg  5711  mptfng  5713  fint  5775  funimass4  5930  fndmdifeq0  6003  funconstss  6015  f1ompt  6059  fconstfv  6143  idref  6164  dff13f  6178  dff14b  6189  weniso  6263  foov  6462  dfwe2  6627  tfis2f  6701  tfindes  6708  frxp  6925  tz7.48lem  7176  tz7.49  7180  oeordi  7306  ixpeq2  7554  ixpin  7565  ixpiin  7566  boxriin  7582  findcard3  7832  fimax2g  7835  fissuni  7897  indexfi  7900  dfsup2  7976  sup0riota  7997  infcllem  8021  wemapsolem  8083  zfinf2  8165  oemapso  8205  zfregs2  8235  r1elss  8295  rankc1  8359  cp  8380  bnd2  8382  aceq1  8566  aceq2  8568  kmlem7  8604  kmlem12  8609  kmlem13  8610  kmlem15  8612  fin12  8861  ac6num  8927  ac6s2  8934  ac6sf  8937  ac6s4  8938  zorn2lem4  8947  zorn2lem6  8949  zorn2lem7  8950  zorng  8952  ttukeylem6  8962  brdom7disj  8977  brdom6disj  8978  fpwwe2  9086  fpwwe  9089  axgroth5  9267  axgroth4  9275  grothprim  9277  nqereu  9372  genpnnp  9448  dfinfre  10610  dfinfmrOLD  10611  infrenegsup  10613  infmsupOLD  10614  infmrgelbOLD  10617  infmrlbOLD  10619  xrsupsslem  11617  xrinfmsslem  11618  xrinfmss2  11621  fzshftral  11908  fsuppmapnn0ub  12245  mptnn0fsuppr  12249  hashgt12el  12636  hashgt12el2  12637  hashbc  12657  cotr2g  13115  rexfiuz  13487  clim0  13647  rpnnen2  14355  gcdcllem1  14552  absproddvds  14666  coprmproddvdslem  14758  vdwmc2  15008  vdwlem13  15022  vdwnn  15027  xpscf  15550  mreacs  15642  acsfn  15643  acsfn1  15645  acsfn2  15647  ispos2  16271  lublecllem  16312  oduglb  16463  odulub  16465  posglbd  16474  isnmnd  16618  gsumwspan  16708  isnsg2  16925  oppgid  17085  oppgcntz  17093  efgval2  17452  iscyggen2  17594  iscyg3  17599  oppr1  17940  isnirred  18006  lssne0  18252  isdomn2  18600  iunocv  19321  islindf4  19473  pmatcollpw2lem  19878  isbasis2g  20040  basdif0  20045  tgval2  20048  ntreq0  20170  isclo2  20181  opnnei  20213  neiptopnei  20225  lmres  20393  ist1-3  20442  cmpcov2  20482  cmpsub  20492  is1stc2  20534  1stccn  20555  kgencn  20648  eltx  20660  txkgen  20744  fbun  20933  trfbas  20937  fbunfip  20962  trfil2  20980  isufil2  21001  fixufil  21015  hausflim  21074  txflf  21099  fclsopn  21107  alexsubALTlem3  21142  iscau3  22326  iscau4  22327  caucfil  22331  bcth3  22377  ovolgelb  22511  dyadmax  22635  itg2leub  22771  itg2cn  22800  plydivex  23329  vieta1  23344  lgseisenlem2  24357  pnt3  24529  tglowdim2ln  24775  axcontlem12  25084  2spotiundisj  25869  frgrareg  25924  frgraregord013  25925  isgrpo2  26006  grpoidinvlem3  26015  nmoubi  26494  lnon0  26520  adjsym  27567  nmopub  27642  nmfnleub  27659  cvbr2  28017  chpssati  28097  chrelat2i  28099  chrelat3  28105  mdsymlem8  28144  ralcom4f  28191  moel  28198  uniinn0  28241  ssiun3  28251  disjnf  28258  disjorf  28266  disjunsn  28281  ac6sf2  28302  nn0min  28459  tosglblem  28505  archiabl  28589  eulerpartlems  29266  eulerpartlemr  29280  eulerpartlemn  29287  ballotlem7  29441  ballotlem7OLD  29479  bnj110  29741  bnj92  29745  bnj539  29774  bnj540  29775  bnj580  29796  bnj978  29832  bnj1047  29854  bnj1128  29871  bnj1417  29922  bnj1421  29923  bnj1312  29939  bnj1498  29942  subfacp1lem3  29977  cvmlift2lem1  30097  cvmlift2lem12  30109  untuni  30408  dfso3  30424  dfpo2  30466  setinds  30495  setinds2f  30496  elpotr  30498  dfon2lem7  30506  dfon2lem9  30508  frins2fg  30556  soseq  30563  nosepon  30627  dfint3  30790  brlb  30793  gtinf  31046  filnetlem4  31108  phpreu  31993  ptrecube  32004  poimirlem1  32005  poimirlem25  32029  poimirlem26  32030  poimirlem27  32031  poimirlem30  32034  mblfinlem2  32042  ftc1anc  32089  inixp  32119  ac6gf  32123  heibor1lem  32205  heiborlem1  32207  iscrngo2  32295  ac6s3f  32478  n0el  32497  lpssat  32650  lssat  32653  lcvbr2  32659  lcvbr3  32660  lfl1  32707  lub0N  32826  glb0N  32830  atlrelat1  32958  hlrelat2  33039  ispsubsp2  33382  pclclN  33527  cdleme25cv  33996  tendoeq2  34412  cdlemk35  34550  setindtrs  35951  cllem0  36241  ss2iundf  36322  undisjrab  36724  zfregs2VD  37300  iunssf  37500  disjinfi  37539  iuneqfzuz  37645  mccl  37775  ioodvbdlimc1lem2  37901  ioodvbdlimc1lem2OLD  37903  ioodvbdlimc2lem  37905  ioodvbdlimc2lemOLD  37906  dvnprodlem3  37920  fourierdlem103  38185  fourierdlem104  38186  sge0iunmpt  38374  hoidmvle  38540  r19.32  38733  2rexrsb  38737  cbvral2  38738  2ralbiim  38740  rmoanim  38745  2rmoswap  38750  2reu3  38754  2reu4a  38755  dfss7  39129  ralnralall  39132  n0snor2el  39143  otiunsndisjX  39152  vtxd0nedgb  39711  pthd  39955  2pthdlem1  40052  3pthdlem1  40078  copisnmnd  40317  lindslinindsimp1  40758  lindslinindsimp2  40764  snlindsntor  40772  ldepslinc  40810  aacllem  41046
  Copyright terms: Public domain W3C validator