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

Theorem rexbii 3070
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.) (Proof shortened by Wolf Lammen, 6-Dec-2019.)
Hypothesis
Ref Expression
rexbii.1 (𝜑𝜓)
Assertion
Ref Expression
rexbii (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓)

Proof of Theorem rexbii
StepHypRef Expression
1 rexbii.1 . . 3 (𝜑𝜓)
21anbi2i 730 . 2 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32rexbii2 3068 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wcel 2030  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-rex 2947
This theorem is referenced by:  2rexbii  3071  rexnal2  3072  ralnex3  3075  r19.29r  3102  r19.29imd  3103  r19.41vv  3120  r19.42v  3121  r19.43  3122  rexcom13  3130  rexrot4  3132  3reeanv  3137  2ralor  3138  cbvrex2v  3210  rexcom4  3256  rexcom4a  3257  rexcom4b  3258  ceqsrex2v  3369  reu7  3434  0el  3972  n0snor2el  4396  uni0b  4495  iuncom  4559  iuncom4  4560  iuniin  4563  dfiunv2  4588  iunab  4598  iunn0  4612  iunin2  4616  iundif2  4619  iunun  4636  iunxiun  4640  iunpwss  4650  inuni  4856  reusv2lem5  4903  reuxfrd  4923  iunopab  5041  dffr2  5108  frc  5109  frminex  5123  dfepfr  5128  epfrc  5129  xpiundi  5207  xpiundir  5208  reliin  5273  iunxpf  5303  cnvuni  5341  dmiun  5365  dfima3  5504  dffr3  5533  rniun  5578  xpdifid  5597  dminxp  5609  imaco  5678  coiun  5683  dffr4  5734  tz6.26  5749  sucel  5836  isarep1  6015  rexrn  6401  ralrn  6402  elrnrexdmb  6404  fnasrn  6451  rexima  6537  ralima  6538  abrexco  6542  imaiun  6543  fliftcnv  6601  rexrnmpt2  6818  iunpw  7020  abrexex2g  7186  abrexex2OLD  7192  el2xptp  7255  rdglem1  7556  tz7.49  7585  oarec  7687  omeu  7710  qsid  7856  eroveu  7885  ixp0  7983  fimax2g  8247  marypha2lem2  8383  dfsup2  8391  infcllem  8434  dfoi  8457  wemapsolem  8496  zfregcl  8540  zfreg  8541  zfregfr  8547  oemapso  8617  zfregs2  8647  infenaleph  8952  isinfcard  8953  kmlem7  9016  kmlem13  9022  fin23lem26  9185  dffin1-5  9248  fin12  9273  numth  9332  ac6n  9345  zorn2lem7  9362  zorng  9364  brdom7disj  9391  brdom6disj  9392  uniwun  9600  axgroth5  9684  axgroth4  9692  grothprim  9694  npomex  9856  genpass  9869  elreal  9990  dfinfre  11042  infrenegsup  11044  uzwo  11789  ublbneg  11811  xrinfmss2  12179  4fvwrd4  12498  fsuppmapnn0fiubex  12832  fsuppmapnn0ub  12835  mptnn0fsuppr  12839  hashge2el2dif  13300  wrdlen1  13376  dfrtrclrec2  13841  rexanuz  14129  rexfiuz  14131  clim0  14281  cbvsum  14469  incexc2  14614  cbvprod  14689  fprodle  14771  iprodmul  14778  divalglem10  15172  divalgb  15174  ncoprmlnprm  15483  phisum  15542  pythagtriplem2  15569  pythagtriplem19  15585  pythagtrip  15586  pceu  15598  prmreclem6  15672  4sqlem12  15707  cshwshashlem1  15849  cshwshash  15858  imasaddfnlem  16235  isdrs2  16986  symgmov1  17858  pmtrprfvalrn  17954  pgpfac1lem5  18524  dvdsrval  18691  opprunit  18707  lsmspsn  19132  lsmelval2  19133  islpidl  19294  mat1dimelbas  20325  mat1dimbas  20326  mdetunilem8  20473  pmatcollpw2lem  20630  tgval2  20808  ntreq0  20929  isclo2  20940  neiptopnei  20984  ist0-3  21197  tgcmp  21252  cmpfi  21259  is1stc2  21293  unisngl  21378  xkobval  21437  txtube  21491  txcmplem1  21492  xkococnlem  21510  eltsms  21983  metrest  22376  iscau3  23122  bcth  23172  pmltpc  23265  itg2i1fseq  23567  itg2cn  23575  plyun0  23998  aaliou3lem9  24150  1cubr  24614  dchrvmasumlema  25234  selbergsb  25309  ostth  25373  istrkg2ld  25404  tglowdim1i  25441  tgdim01  25447  legtrid  25531  midex  25674  ishpg  25696  brbtwn2  25830  colinearalg  25835  ax5seg  25863  axpasch  25866  axlowdimlem6  25872  axeuclidlem  25887  axeuclid  25888  umgr2edg1  26148  umgr2edgneu  26151  nbgrsym  26308  nbgrsymOLD  26309  isuvtx  26343  isuvtxaOLD  26344  usgr2pth0  26717  wlkiswwlksupgr2  26831  clwwlknun  27087  clwwlknunOLD  27091  4cycl2vnunb  27270  fusgreg2wsp  27316  lpni  27462  nmobndseqi  27762  hhcmpl  28185  shne0i  28435  nmcopexi  29014  nmcfnexi  29038  cdj3lem3b  29427  rexcom4f  29445  iunin1f  29500  ofpreima  29593  fpwrelmapffslem  29635  tosglblem  29797  xrnarchi  29866  ordtconnlem1  30098  lmdvg  30127  esumfsup  30260  reprsuc  30821  reprdifc  30833  bnj168  30924  bnj1185  30990  bnj1542  31053  bnj865  31119  bnj916  31129  bnj983  31147  bnj1176  31199  bnj1189  31203  bnj1296  31215  bnj1398  31228  bnj1450  31244  bnj1463  31249  cvmliftlem15  31406  cvmlift2lem12  31422  dffr5  31769  imaindm  31806  dfon2lem9  31820  frpomin2  31864  soseq  31879  noseponlem  31942  nosepon  31943  nolt02o  31970  brbigcup  32130  elfuns  32147  brimage  32158  brimg  32169  dfrecs2  32182  imagesset  32185  brub  32186  brsegle  32340  gtinfOLD  32439  filnetlem4  32501  bj-rexcom4a  32995  bj-rexcom4bv  32996  bj-rexcom4b  32997  bj-elsngl  33081  bj-rest10  33166  bj-restreg  33177  bj-mpt2mptALT  33197  iundif1  33513  matunitlindflem1  33535  poimirlem1  33540  poimirlem30  33569  poimirlem32  33571  poimir  33572  ismblfin  33580  volsupnfl  33584  itg2addnclem3  33593  fdc  33671  isfldidl  33997  eldmqsres2  34193  n0elqs  34239  rnxrncnvepres  34298  rnxrnidres  34299  dfcoels  34325  br1cossinres  34337  br1cossinidres  34339  br1cossincnvepres  34340  br1cossxrnidres  34341  br1cossxrncnvepres  34342  br1cossxrncnvssrres  34398  prtlem10  34469  prter2  34485  islshpat  34622  lshpsmreu  34714  2dim  35074  islpln5  35139  lplnexatN  35167  islvol5  35183  dalem18  35285  dalem20  35297  lhpexle2  35614  lhpexle3  35616  lhpex2leN  35617  4atex2  35681  4atex2-0bOLDN  35683  cdlemftr3  36170  cdlemg17pq  36277  cdlemg19  36289  cdlemg21  36291  cdlemg33d  36314  dva1dim  36590  dih1dimatlem  36935  dihglb2  36948  dvh2dim  37051  mapdrvallem2  37251  mapdpglem3  37281  hdmapglem7a  37536  elrfirn  37575  isnacs2  37586  isnacs3  37590  sbc2rex  37668  4rexfrabdioph  37679  eldioph4b  37692  fphpd  37697  fiphp3d  37700  rencldnfilem  37701  rmxdioph  37900  expdiophlem1  37905  islnm2  37965  elimaint  38257  cnviun  38259  imaiun1  38260  coiun1  38261  elintima  38262  briunov2  38291  clsk3nimkb  38655  prmunb2  38827  zfregs2VD  39390  evth2f  39488  evthf  39500  ndisj2  39532  fnlimabslt  40229  climbddf  40237  limsupub  40254  limsuppnflem  40260  limsupubuz  40263  limsupre2lem  40274  limsupreuz  40287  limsupvaluz2  40288  cnrefiisplem  40373  cnrefiisp  40374  stoweidlem28  40563  fourierdlem63  40704  fourierdlem65  40706  fourierdlem89  40730  fourierdlem90  40731  fourierdlem91  40732  fourierdlem100  40741  sge0pnfmpt  40980  ovn0  41101  smfaddlem1  41292  smflimlem4  41303  2rexsb  41491  2rexrsb  41492  cbvrex2  41494  2reu5a  41498  copisnmnd  42134  pgrpgt2nabl  42472  islindeps  42567  lindslinindsimp1  42571  lindslinindsimp2  42577  islindeps2  42597  islininds2  42598  isldepslvec2  42599  ldepslinc  42623
  Copyright terms: Public domain W3C validator