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

Theorem rexbii 2847
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
rexbii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
rexbii  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )

Proof of Theorem rexbii
StepHypRef Expression
1 rexbii.1 . . . 4  |-  ( ph  <->  ps )
21a1i 11 . . 3  |-  ( T. 
->  ( ph  <->  ps )
)
32rexbidv 2844 . 2  |-  ( T. 
->  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
)
43trud 1379 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   T. wtru 1371   E.wrex 2796
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-rex 2801
This theorem is referenced by:  2rexbii  2848  rexanali  2870  r19.29r  2954  r19.29imd  2955  r19.41vv  2970  r19.42v  2971  r19.43  2972  rexcom13  2979  rexrot4  2980  3reeanv  2985  2ralor  2986  cbvrex2v  3052  rexcom4  3088  rexcom4a  3089  rexcom4b  3090  ceqsrex2v  3192  reu7  3251  0el  3752  uni0b  4214  iuncom  4275  iuncom4  4276  iuniin  4279  dfiunv2  4304  iunab  4314  iunn0  4328  iunin2  4332  iundif2  4335  iunun  4349  iunxiun  4351  iunpwss  4358  inuni  4552  reusv2lem5  4595  reusv5OLD  4600  reusv7OLD  4602  reuxfrd  4615  iunopab  4722  dffr2  4783  frc  4784  frminex  4798  dfepfr  4803  epfrc  4804  sucel  4890  xpiundi  4991  xpiundir  4992  reliin  5059  iunxpf  5086  cnvuni  5124  dmiun  5146  dfima3  5270  dffr3  5299  rniun  5345  xpdifid  5364  dminxp  5376  imaco  5441  coiun  5445  isarep1  5595  rexrn  5944  ralrn  5945  elrnrexdmb  5947  fnasrn  5987  rexima  6055  ralima  6056  abrexco  6060  imaiun  6061  fliftcnv  6103  rexrnmpt2  6306  iunpw  6490  abrexex2g  6654  abrexex2  6658  rdglem1  6971  tz7.49  7000  oarec  7101  omeu  7124  qsid  7266  eroveu  7295  ixp0  7396  fimax2g  7659  marypha2lem2  7787  dfsup2  7793  dfsup2OLD  7794  dfoi  7826  wemapsolem  7865  zfregcl  7910  zfreg  7911  zfreg2  7912  oemapso  7991  zfregs2  8054  infenaleph  8362  isinfcard  8363  kmlem7  8426  kmlem13  8432  fin23lem26  8595  dffin1-5  8658  fin12  8683  numth  8742  ac6n  8755  zorn2lem7  8772  zorng  8774  brdom7disj  8799  brdom6disj  8800  uniwun  9008  axgroth5  9092  axgroth4  9100  grothprim  9102  npomex  9266  genpass  9279  elreal  9399  dfinfmr  10408  infmsup  10409  infmrgelb  10411  infmrlb  10412  uzwo  11018  uzwoOLD  11019  ublbneg  11040  xrinfmss2  11374  4fvwrd4  11634  hashge2el2dif  12286  rexanuz  12935  rexfiuz  12937  clim0  13086  cbvsum  13274  incexc2  13403  divalglem10  13708  divalgb  13710  pythagtriplem2  13986  pythagtriplem19  14002  pythagtrip  14003  pceu  14015  prmreclem6  14084  4sqlem12  14119  cshwshashlem1  14224  cshwshash  14233  imasaddfnlem  14568  isdrs2  15211  symgmov1  15999  symgmov2  16000  pmtrprfvalrn  16096  pgpfac1lem5  16685  dvdsrval  16843  opprunit  16859  lsmspsn  17271  lsmelval2  17272  islpidl  17434  mdetunilem8  18541  tgval2  18677  ntreq0  18797  isclo2  18808  neiptopnei  18852  ist0-3  19065  tgcmp  19120  cmpfi  19127  is1stc2  19162  xkobval  19275  txtube  19329  txcmplem1  19330  xkococnlem  19348  eltsms  19819  metrest  20215  iscau3  20905  bcth  20956  pmltpc  21050  itg2i1fseq  21349  itg2cn  21357  plyun0  21781  aaliou3lem9  21932  1cubr  22353  dchrvmasumlema  22865  selbergsb  22940  ostth  23004  istrkg2ld  23038  tglowdim1i  23072  tgdim01  23078  legtrid  23143  mideu  23245  brbtwn2  23286  colinearalg  23291  ax5seg  23319  axpasch  23322  axlowdimlem6  23328  axeuclidlem  23343  axeuclid  23344  usgra2edg1  23437  nbgraop1  23471  nbgraf1olem1  23485  lpni  23801  isgrpo2  23819  isgrp2d  23857  nmobndseqi  24314  hhcmpl  24737  shne0i  24986  nmcopexi  25566  nmcfnexi  25590  cdj3lem3b  25979  rexcom4f  25996  disjunsn  26070  ofpreima  26118  fpwrelmapffslem  26166  tosglblem  26264  xrnarchi  26335  archiabl  26349  ordtconlem1  26488  lmdvg  26517  esumfsup  26653  cvmliftlem15  27321  cvmlift2lem12  27337  dfrtrclrec2  27479  cbvprod  27562  iprodmul  27637  dffr5  27697  dfon2lem9  27738  dffr4  27777  tz6.26  27800  soseq  27849  nodenselem4  27959  nodenselem5  27960  nofulllem5  27981  brbigcup  28063  elfuns  28080  brimage  28091  brimg  28102  tfrqfree  28116  imagesset  28118  brub  28119  brsegle  28273  iundif1  28551  ismblfin  28570  volsupnfl  28574  itg2addnclem3  28583  gtinf  28652  nn0prpw  28656  filnetlem4  28740  fdc  28779  smprngopr  28990  isfldidl  29006  prtlem10  29148  prter2  29164  elrfirn  29169  isnacs2  29180  isnacs3  29184  sbc2rex  29263  4rexfrabdioph  29274  eldioph4b  29288  fphpd  29293  fiphp3d  29296  rencldnfilem  29297  rmxdioph  29503  expdiophlem1  29508  islnm2  29569  phisum  29705  evth2f  29875  evthf  29887  stoweidlem28  29961  2rexsb  30132  2rexrsb  30133  cbvrex2  30135  2reu5a  30139  el2xptp  30264  rabasiun  30368  wrdlen1  30388  usgra2pth0  30440  el2wlkonot  30526  el2spthonot  30527  el2wlkonotot0  30529  4cycl2vnunb  30747  vdn0frgrav2  30754  vdgn0frgrav2  30755  usg2spot2nb  30796  usgreg2spot  30798  numclwwlkun  30810  pgrpgt2nabel  30909  fsuppmapnn0ub  30934  fsuppmapnn0fiubex  30938  mptnn0fsuppr  30941  mat1dimelbas  31021  mat1dimbas  31022  islindeps  31094  lindslinindsimp1  31098  lindslinindsimp2  31104  islindeps2  31124  islininds2  31125  isldepslvec2  31126  ldepslinc  31158  pmatcollpwlem  31233  zfregs2VD  31877  bnj168  32021  bnj1185  32087  bnj1542  32150  bnj865  32216  bnj916  32226  bnj983  32244  bnj1176  32296  bnj1189  32300  bnj1296  32312  bnj1398  32325  bnj1450  32341  bnj1463  32346  bj-rexcom4a  32681  bj-rexcom4bv  32682  bj-rexcom4b  32683  bj-elsngl  32761  islshpat  32968  lshpsmreu  33060  2dim  33420  islpln5  33485  lplnexatN  33513  islvol5  33529  dalem18  33631  dalem20  33643  lhpexle2  33960  lhpexle3  33962  lhpex2leN  33963  4atex2  34027  4atex2-0bOLDN  34029  cdlemftr3  34515  cdlemg17pq  34622  cdlemg19  34634  cdlemg21  34636  cdlemg33d  34659  dva1dim  34935  dih1dimatlem  35280  dihglb2  35293  dvh2dim  35396  mapdrvallem2  35596  mapdpglem3  35626  hdmapglem7a  35881
  Copyright terms: Public domain W3C validator