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

Theorem ralbii 2744
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.)
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 . . . 4  |-  ( ph  <->  ps )
21a1i 11 . . 3  |-  ( T. 
->  ( ph  <->  ps )
)
32ralbidv 2740 . 2  |-  ( T. 
->  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )
)
43trud 1378 1  |-  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   T. wtru 1370   A.wral 2720
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-ral 2725
This theorem is referenced by:  2ralbii  2746  ralinexa  2765  nrexralim  2767  r3al  2778  r19.26-2  2855  r19.26-3  2856  ralbiim  2859  r19.28av  2861  r19.30  2870  r19.32v  2871  r19.35  2872  cbvral2v  2960  cbvral3v  2962  sbralie  2965  ralcom4  2996  ralxpxfr2d  3089  reu8  3160  2reuswap  3166  2reu5lem2  3170  eqsn  4039  uni0b  4121  uni0c  4122  ssint  4149  iuniin  4186  iuneq2  4192  iunss  4216  ssiinf  4224  iinab  4236  iinun2  4241  iindif2  4244  iinin2  4245  iinuni  4259  sspwuni  4261  iinpw  4264  disjor  4281  disjxun  4295  dftr3  4394  trint  4405  reusv3  4505  reusv5OLD  4507  reuxfr2d  4520  ssrel2  4935  reliun  4965  xpiindi  4980  rexiunxp  4985  ralxpf  4991  rexxpf  4992  dfse2  5207  asymref2  5220  rninxp  5282  dminxp  5283  cnviin  5379  cnvpo  5380  dffun9  5451  funcnv3  5484  fncnv  5487  fnres  5532  fnopabg  5539  mptfng  5541  fint  5595  funimass4  5747  fndmdifeq0  5814  funconstss  5826  f1ompt  5870  idref  5963  dff13f  5978  weniso  6050  foov  6242  dfwe2  6398  tfis2f  6471  tfindes  6478  frxp  6687  tz7.48lem  6901  tz7.49  6905  oeordi  7031  ixpeq2  7282  ixpin  7293  ixpiin  7294  boxriin  7310  findcard3  7560  fimax2g  7563  fissuni  7621  indexfi  7624  dfsup2  7697  wemapsolem  7769  zfinf2  7853  oemapso  7895  zfregs2  7958  r1elss  8018  rankc1  8082  cp  8103  bnd2  8105  aceq1  8292  aceq2  8294  kmlem7  8330  kmlem12  8335  kmlem13  8336  kmlem15  8338  fin12  8587  ac6num  8653  ac6s2  8660  ac6sf  8663  ac6s4  8664  zorn2lem4  8673  zorn2lem6  8675  zorn2lem7  8676  zorng  8678  ttukeylem6  8688  brdom7disj  8703  brdom6disj  8704  fpwwe2  8815  fpwwe  8818  axgroth5  8996  axgroth4  9004  grothprim  9006  nqereu  9103  genpnnp  9179  dfinfmr  10312  infmsup  10313  infmrgelb  10315  infmrlb  10316  xrsupsslem  11274  xrinfmsslem  11275  xrinfmss2  11278  fzshftral  11552  hashgt12el  12178  hashgt12el2  12179  hashbc  12211  rexfiuz  12840  clim0  12989  rpnnen2  13513  gcdcllem1  13700  vdwmc2  14045  vdwlem13  14059  vdwnn  14064  xpscf  14509  mreacs  14601  acsfn  14602  acsfn1  14604  acsfn2  14606  ispos2  15123  lublecllem  15163  oduglb  15314  odulub  15316  posglbd  15325  gsumwspan  15529  isnsg2  15716  oppgid  15876  oppgcntz  15884  efgval2  16226  iscyggen2  16363  iscyg3  16368  oppr1  16731  isnirred  16797  lssne0  17037  isdomn2  17376  iunocv  18111  islindf4  18272  isbasis2g  18558  basdif0  18563  tgval2  18566  ntreq0  18686  isclo2  18697  opnnei  18729  neiptopnei  18741  lmres  18909  ist1-3  18958  cmpcov2  18998  cmpsub  19008  is1stc2  19051  1stccn  19072  kgencn  19134  eltx  19146  txkgen  19230  fbun  19418  trfbas  19422  fbunfip  19447  trfil2  19465  isufil2  19486  fixufil  19500  hausflim  19559  txflf  19584  fclsopn  19592  alexsubALTlem3  19626  iscau3  20794  iscau4  20795  caucfil  20799  bcth3  20847  ovolgelb  20968  dyadmax  21083  itg2leub  21217  itg2cn  21246  plydivex  21768  vieta1  21783  lgseisenlem2  22694  pnt3  22866  axcontlem12  23226  isgrpo2  23689  grpoidinvlem3  23698  nmoubi  24177  lnon0  24203  adjsym  25242  nmopub  25317  nmfnleub  25334  cvbr2  25692  chpssati  25772  chrelat2i  25774  chrelat3  25780  mdsymlem8  25819  ralcom4f  25865  moel  25872  ssiun3  25914  disjnf  25921  disjorf  25928  disjunsn  25941  mptfnf  25981  nn0min  26095  tosglblem  26135  archiabl  26220  eulerpartlems  26748  eulerpartlemr  26762  eulerpartlemn  26769  ballotlem7  26923  subfacp1lem3  27075  cvmlift2lem1  27196  cvmlift2lem12  27208  untuni  27365  dfso3  27381  dfpo2  27570  setinds  27596  setinds2f  27597  elpotr  27599  dfon2lem7  27607  dfon2lem9  27609  wfis2fg  27677  frins2fg  27713  soseq  27720  dfint3  27988  brlb  27991  mblfinlem2  28434  ftc1anc  28480  gtinf  28519  filnetlem4  28607  inixp  28627  ac6gf  28631  heibor1lem  28713  heiborlem1  28715  iscrngo2  28803  ac6s3f  28988  n0el  29009  setindtrs  29379  r19.32  29996  2rexrsb  30000  cbvral2  30001  2ralbiim  30003  rmoanim  30008  2rmoswap  30013  2reu3  30017  2reu4a  30018  ralnralall  30123  raldifsnb  30128  otiunsndisj  30137  otiunsndisjX  30138  dff14b  30150  2spotiundisj  30660  frgrareg  30715  frgraregord013  30716  fsuppmapnn0ub  30801  pmatcollpw2lem  30910  lindslinindsimp1  30996  lindslinindsimp2  31002  snlindsntor  31010  ldepslinc  31056  zfregs2VD  31582  bnj110  31856  bnj92  31860  bnj539  31889  bnj540  31890  bnj580  31911  bnj978  31947  bnj1047  31969  bnj1128  31986  bnj1417  32037  bnj1421  32038  bnj1312  32054  bnj1498  32057  lpssat  32663  lssat  32666  lcvbr2  32672  lcvbr3  32673  lfl1  32720  lub0N  32839  glb0N  32843  atlrelat1  32971  hlrelat2  33052  ispsubsp2  33395  pclclN  33540  cdleme25cv  34007  tendoeq2  34423  cdlemk35  34561
  Copyright terms: Public domain W3C validator