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

Theorem rexbii 2722
Description: Inference adding restricted existential 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
rexbii  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )

Proof of Theorem rexbii
StepHypRef Expression
1 ralbii.1 . . . 4  |-  ( ph  <->  ps )
21a1i 11 . . 3  |-  (  T. 
->  ( ph  <->  ps )
)
32rexbidv 2718 . 2  |-  (  T. 
->  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
)
43trud 1332 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    T. wtru 1325   E.wrex 2698
This theorem is referenced by:  2rexbii  2724  rexanali  2743  r19.29r  2839  r19.42v  2854  r19.43  2855  rexcom13  2862  rexrot4  2863  3reeanv  2868  2ralor  2869  cbvrex2v  2933  rexcom4  2967  rexcom4a  2968  rexcom4b  2969  ceqsrex2v  3063  reu7  3121  0el  3636  uni0b  4032  iuncom  4091  iuncom4  4092  iuniin  4095  dfiunv2  4119  iunab  4129  iunn0  4143  iunin2  4147  iundif2  4150  iunun  4163  iunxiun  4165  iunpwss  4172  inuni  4354  iunopab  4478  dffr2  4539  frc  4540  frminex  4554  dfepfr  4559  epfrc  4560  sucel  4646  reusv2lem5  4720  reusv5OLD  4725  reusv7OLD  4727  reuxfrd  4740  iunpw  4751  xpiundi  4924  xpiundir  4925  reliin  4988  iunxpf  5013  cnvuni  5049  dmiun  5070  dfima3  5198  dffr3  5228  rniun  5274  dminxp  5303  imaco  5367  coiun  5371  isarep1  5524  rexrn  5864  ralrn  5865  elrnrexdmb  5867  fnasrn  5904  rexima  5969  ralima  5970  abrexco  5978  abrexex2g  5980  imaiun  5984  abrexex2  5993  fliftcnv  6025  rexrnmpt2  6177  rdglem1  6665  tz7.49  6694  oarec  6797  omeu  6820  qsid  6962  eroveu  6991  ixp0  7087  fimax2g  7345  marypha2lem2  7433  dfsup2  7439  dfsup2OLD  7440  dfoi  7472  wemapso2lem  7511  zfregcl  7554  zfreg  7555  zfreg2  7556  oemapso  7630  zfregs2  7661  infenaleph  7964  isinfcard  7965  kmlem7  8028  kmlem13  8034  fin23lem26  8197  dffin1-5  8260  fin12  8285  numth  8344  ac6n  8357  zorn2lem7  8374  zorng  8376  brdom7disj  8401  brdom6disj  8402  uniwun  8607  axgroth5  8691  axgroth4  8699  grothprim  8701  npomex  8865  genpass  8878  elreal  8998  dfinfmr  9977  infmsup  9978  infmrgelb  9980  infmrlb  9981  uzwo  10531  uzwoOLD  10532  ublbneg  10552  xrinfmss2  10881  4fvwrd4  11113  rexanuz  12141  rexfiuz  12143  clim0  12292  incexc2  12610  divalglem10  12914  divalgb  12916  pythagtriplem2  13183  pythagtriplem19  13199  pythagtrip  13200  pceu  13212  prmreclem6  13281  4sqlem12  13316  imasaddfnlem  13745  isdrs2  14388  pgpfac1lem5  15629  dvdsrval  15742  opprunit  15758  lsmspsn  16148  lsmelval2  16149  islpidl  16309  tgval2  17013  ntreq0  17133  isclo2  17144  neiptopnei  17188  ist0-3  17401  tgcmp  17456  cmpfi  17463  is1stc2  17497  xkobval  17610  txtube  17664  txcmplem1  17665  xkococnlem  17683  eltsms  18154  metrest  18546  iscau3  19223  bcth  19274  pmltpc  19339  itg2i1fseq  19639  itg2cn  19647  plyun0  20108  aaliou3lem9  20259  1cubr  20674  dchrvmasumlema  21186  selbergsb  21261  ostth  21325  usgra2edg1  21395  nbgraop1  21429  nbgraf1olem1  21443  lpni  21759  isgrpo2  21777  isgrp2d  21815  nmobndseqi  22272  hhcmpl  22694  shne0i  22942  nmcopexi  23522  nmcfnexi  23546  cdj3lem3b  23935  rexcom4f  23958  r19.41vv  23962  ofpreima  24073  tosglb  24184  xrnarchi  24246  lmdvg  24330  esumfsup  24452  cvmliftlem15  24977  cvmlift2lem12  24993  dfrtrclrec2  25135  cbvprod  25233  iprodmul  25308  dffr5  25368  dfon2lem9  25410  dffr4  25449  tz6.26  25472  soseq  25521  nodenselem4  25631  nodenselem5  25632  nofulllem5  25653  brbigcup  25735  elfuns  25752  brimage  25763  brimg  25774  tfrqfree  25788  imagesset  25790  brub  25791  brbtwn2  25836  colinearalg  25841  ax5seg  25869  axpasch  25872  axlowdimlem6  25878  axeuclidlem  25893  axeuclid  25894  brsegle  26034  ismblfin  26237  volsupnfl  26241  itg2addnclem3  26248  gtinf  26313  nn0prpw  26317  filnetlem4  26401  fdc  26440  smprngopr  26653  isfldidl  26669  prtlem10  26705  prter2  26721  elrfirn  26740  isnacs2  26751  isnacs3  26755  4rexfrabdioph  26849  eldioph4b  26863  fphpd  26868  fiphp3d  26871  rencldnfilem  26872  rmxdioph  27078  expdiophlem1  27083  islnm2  27144  phisum  27486  evth2f  27653  evthf  27665  stoweidlem28  27744  2rexsb  27915  2rexrsb  27916  cbvrex2  27918  2reu5a  27922  el2xptp  28050  cshwssizelem3  28245  cshwssize  28253  usgra2pth0  28265  el2wlkonot  28289  el2spthonot  28290  el2wlkonotot0  28292  4cycl2vnunb  28344  vdn0frgrav2  28351  vdgn0frgrav2  28352  usg2spot2nb  28391  usgreg2spot  28393  zfregs2VD  28890  bnj168  29034  bnj1185  29102  bnj1542  29165  bnj865  29231  bnj916  29241  bnj983  29259  bnj1176  29311  bnj1189  29315  bnj1296  29327  bnj1398  29340  bnj1450  29356  bnj1463  29361  islshpat  29752  lshpsmreu  29844  2dim  30204  islpln5  30269  lplnexatN  30297  islvol5  30313  dalem18  30415  dalem20  30427  lhpexle2  30744  lhpexle3  30746  lhpex2leN  30747  4atex2  30811  4atex2-0bOLDN  30813  cdlemftr3  31299  cdlemg17pq  31406  cdlemg19  31418  cdlemg21  31420  cdlemg33d  31443  dva1dim  31719  dih1dimatlem  32064  dihglb2  32077  dvh2dim  32180  mapdrvallem2  32380  mapdpglem3  32410  hdmapglem7a  32665
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-rex 2703
  Copyright terms: Public domain W3C validator