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

Theorem rexbii 2730
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 2726 . 2  |-  ( T. 
->  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
)
43trud 1371 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   T. wtru 1363   E.wrex 2706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-rex 2711
This theorem is referenced by:  2rexbii  2732  rexanali  2751  r19.29r  2848  r19.29imd  2849  r19.41vv  2864  r19.42v  2865  r19.43  2866  rexcom13  2873  rexrot4  2874  3reeanv  2879  2ralor  2880  cbvrex2v  2946  rexcom4  2982  rexcom4a  2983  rexcom4b  2984  ceqsrex2v  3084  reu7  3143  0el  3642  uni0b  4104  iuncom  4165  iuncom4  4166  iuniin  4169  dfiunv2  4194  iunab  4204  iunn0  4218  iunin2  4222  iundif2  4225  iunun  4239  iunxiun  4241  iunpwss  4248  inuni  4442  reusv2lem5  4485  reusv5OLD  4490  reusv7OLD  4492  reuxfrd  4505  iunopab  4611  dffr2  4672  frc  4673  frminex  4687  dfepfr  4692  epfrc  4693  sucel  4779  xpiundi  4880  xpiundir  4881  reliin  4948  iunxpf  4975  cnvuni  5013  dmiun  5035  dfima3  5160  dffr3  5189  rniun  5235  xpdifid  5254  dminxp  5266  imaco  5331  coiun  5335  isarep1  5485  rexrn  5833  ralrn  5834  elrnrexdmb  5836  fnasrn  5875  rexima  5943  ralima  5944  abrexco  5948  imaiun  5949  fliftcnv  5991  rexrnmpt2  6195  iunpw  6379  abrexex2g  6543  abrexex2  6547  rdglem1  6857  tz7.49  6886  oarec  6989  omeu  7012  qsid  7154  eroveu  7183  ixp0  7284  fimax2g  7546  marypha2lem2  7674  dfsup2  7680  dfsup2OLD  7681  dfoi  7713  wemapsolem  7752  zfregcl  7797  zfreg  7798  zfreg2  7799  oemapso  7878  zfregs2  7941  infenaleph  8249  isinfcard  8250  kmlem7  8313  kmlem13  8319  fin23lem26  8482  dffin1-5  8545  fin12  8570  numth  8629  ac6n  8642  zorn2lem7  8659  zorng  8661  brdom7disj  8686  brdom6disj  8687  uniwun  8895  axgroth5  8979  axgroth4  8987  grothprim  8989  npomex  9153  genpass  9166  elreal  9286  dfinfmr  10295  infmsup  10296  infmrgelb  10298  infmrlb  10299  uzwo  10905  uzwoOLD  10906  ublbneg  10927  xrinfmss2  11261  4fvwrd4  11517  hashge2el2dif  12168  rexanuz  12817  rexfiuz  12819  clim0  12968  cbvsum  13156  incexc2  13284  divalglem10  13589  divalgb  13591  pythagtriplem2  13867  pythagtriplem19  13883  pythagtrip  13884  pceu  13896  prmreclem6  13965  4sqlem12  14000  cshwshashlem1  14105  cshwshash  14114  imasaddfnlem  14449  isdrs2  15092  symgmov1  15877  symgmov2  15878  pmtrprfvalrn  15974  pgpfac1lem5  16554  dvdsrval  16671  opprunit  16687  lsmspsn  17087  lsmelval2  17088  islpidl  17250  mdetunilem8  18267  tgval2  18403  ntreq0  18523  isclo2  18534  neiptopnei  18578  ist0-3  18791  tgcmp  18846  cmpfi  18853  is1stc2  18888  xkobval  19001  txtube  19055  txcmplem1  19056  xkococnlem  19074  eltsms  19545  metrest  19941  iscau3  20631  bcth  20682  pmltpc  20776  itg2i1fseq  21075  itg2cn  21083  plyun0  21550  aaliou3lem9  21701  1cubr  22122  dchrvmasumlema  22634  selbergsb  22709  ostth  22773  tglowdim1i  22836  legtrid  22898  brbtwn2  22974  colinearalg  22979  ax5seg  23007  axpasch  23010  axlowdimlem6  23016  axeuclidlem  23031  axeuclid  23032  usgra2edg1  23125  nbgraop1  23159  nbgraf1olem1  23173  lpni  23489  isgrpo2  23507  isgrp2d  23545  nmobndseqi  24002  hhcmpl  24425  shne0i  24674  nmcopexi  25254  nmcfnexi  25278  cdj3lem3b  25667  rexcom4f  25684  disjunsn  25760  ofpreima  25808  fpwrelmapffslem  25857  tosglblem  25953  xrnarchi  26025  archiabl  26039  ordtconlem1  26208  lmdvg  26237  esumfsup  26373  cvmliftlem15  27035  cvmlift2lem12  27051  dfrtrclrec2  27192  cbvprod  27275  iprodmul  27350  dffr5  27410  dfon2lem9  27451  dffr4  27490  tz6.26  27513  soseq  27562  nodenselem4  27672  nodenselem5  27673  nofulllem5  27694  brbigcup  27776  elfuns  27793  brimage  27804  brimg  27815  tfrqfree  27829  imagesset  27831  brub  27832  brsegle  27986  iundif1  28257  ismblfin  28276  volsupnfl  28280  itg2addnclem3  28289  gtinf  28358  nn0prpw  28362  filnetlem4  28446  fdc  28485  smprngopr  28696  isfldidl  28712  prtlem10  28855  prter2  28871  elrfirn  28876  isnacs2  28887  isnacs3  28891  sbc2rex  28970  4rexfrabdioph  28981  eldioph4b  28995  fphpd  29000  fiphp3d  29003  rencldnfilem  29004  rmxdioph  29210  expdiophlem1  29215  islnm2  29276  phisum  29412  evth2f  29582  evthf  29594  stoweidlem28  29669  2rexsb  29840  2rexrsb  29841  cbvrex2  29843  2reu5a  29847  el2xptp  29972  rabasiun  30076  wrdlen1  30096  usgra2pth0  30148  el2wlkonot  30234  el2spthonot  30235  el2wlkonotot0  30237  4cycl2vnunb  30455  vdn0frgrav2  30462  vdgn0frgrav2  30463  usg2spot2nb  30504  usgreg2spot  30506  numclwwlkun  30518  pgrpgt2nabel  30600  islindeps  30696  lindslinindsimp1  30700  lindslinindsimp2  30706  islindeps2  30726  islininds2  30727  isldepslvec2  30728  ldepslinc  30760  zfregs2VD  31279  bnj168  31423  bnj1185  31489  bnj1542  31552  bnj865  31618  bnj916  31628  bnj983  31646  bnj1176  31698  bnj1189  31702  bnj1296  31714  bnj1398  31727  bnj1450  31743  bnj1463  31748  bj-rexcom4a  31986  bj-rexcom4b  31987  bj-elsngl  32044  islshpat  32235  lshpsmreu  32327  2dim  32687  islpln5  32752  lplnexatN  32780  islvol5  32796  dalem18  32898  dalem20  32910  lhpexle2  33227  lhpexle3  33229  lhpex2leN  33230  4atex2  33294  4atex2-0bOLDN  33296  cdlemftr3  33782  cdlemg17pq  33889  cdlemg19  33901  cdlemg21  33903  cdlemg33d  33926  dva1dim  34202  dih1dimatlem  34547  dihglb2  34560  dvh2dim  34663  mapdrvallem2  34863  mapdpglem3  34893  hdmapglem7a  35148
  Copyright terms: Public domain W3C validator