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

Theorem rexbii 3023
 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 726 . 2 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32rexbii2 3021 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∈ wcel 1977  ∃wrex 2897 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-rex 2902 This theorem is referenced by:  2rexbii  3024  rexnal2  3025  ralnex3  3028  r19.29r  3055  r19.29imd  3056  r19.41vv  3072  r19.42v  3073  r19.43  3074  rexcom13  3081  rexrot4  3082  3reeanv  3087  2ralor  3088  cbvrex2v  3156  rexcom4  3198  rexcom4a  3199  rexcom4b  3200  ceqsrex2v  3308  reu7  3368  0el  3895  n0snor2el  4304  uni0b  4399  rabasiun  4459  iuncom  4463  iuncom4  4464  iuniin  4467  dfiunv2  4492  iunab  4502  iunn0  4516  iunin2  4520  iundif2  4523  iunun  4540  iunxiun  4544  iunpwss  4551  inuni  4753  reusv2lem5  4799  reuxfrd  4819  iunopab  4936  dffr2  5003  frc  5004  frminex  5018  dfepfr  5023  epfrc  5024  xpiundi  5096  xpiundir  5097  reliin  5163  iunxpf  5192  cnvuni  5231  dmiun  5255  dfima3  5388  dffr3  5417  rniun  5462  xpdifid  5481  dminxp  5493  imaco  5557  coiun  5562  dffr4  5613  tz6.26  5628  sucel  5715  isarep1  5891  rexrn  6269  ralrn  6270  elrnrexdmb  6272  fnasrn  6317  rexima  6401  ralima  6402  abrexco  6406  imaiun  6407  fliftcnv  6461  rexrnmpt2  6674  iunpw  6870  abrexex2g  7036  abrexex2  7040  el2xptp  7102  rdglem1  7398  tz7.49  7427  oarec  7529  omeu  7552  qsid  7700  eroveu  7729  ixp0  7827  fimax2g  8091  marypha2lem2  8225  dfsup2  8233  infcllem  8276  dfoi  8299  wemapsolem  8338  zfregcl  8382  zfreg  8383  zfregclOLD  8384  zfregOLD  8385  zfreg2OLD  8386  zfregfr  8392  oemapso  8462  zfregs2  8492  infenaleph  8797  isinfcard  8798  kmlem7  8861  kmlem13  8867  fin23lem26  9030  dffin1-5  9093  fin12  9118  numth  9177  ac6n  9190  zorn2lem7  9207  zorng  9209  brdom7disj  9234  brdom6disj  9235  uniwun  9441  axgroth5  9525  axgroth4  9533  grothprim  9535  npomex  9697  genpass  9710  elreal  9831  dfinfre  10881  infrenegsup  10883  uzwo  11627  ublbneg  11649  xrinfmss2  12013  4fvwrd4  12328  fsuppmapnn0fiubex  12654  fsuppmapnn0ub  12657  mptnn0fsuppr  12661  hashge2el2dif  13117  wrdlen1  13198  dfrtrclrec2  13645  rexanuz  13933  rexfiuz  13935  clim0  14085  cbvsum  14273  incexc2  14409  cbvprod  14484  fprodle  14566  iprodmul  14573  divalglem10  14963  divalgb  14965  ncoprmlnprm  15274  phisum  15333  pythagtriplem2  15360  pythagtriplem19  15376  pythagtrip  15377  pceu  15389  prmreclem6  15463  4sqlem12  15498  cshwshashlem1  15640  cshwshash  15649  imasaddfnlem  16011  isdrs2  16762  symgmov1  17635  pmtrprfvalrn  17731  pgpfac1lem5  18301  dvdsrval  18468  opprunit  18484  lsmspsn  18905  lsmelval2  18906  islpidl  19067  mat1dimelbas  20096  mat1dimbas  20097  mdetunilem8  20244  pmatcollpw2lem  20401  tgval2  20571  ntreq0  20691  isclo2  20702  neiptopnei  20746  ist0-3  20959  tgcmp  21014  cmpfi  21021  is1stc2  21055  unisngl  21140  xkobval  21199  txtube  21253  txcmplem1  21254  xkococnlem  21272  eltsms  21746  metrest  22139  iscau3  22884  bcth  22934  pmltpc  23026  itg2i1fseq  23328  itg2cn  23336  plyun0  23757  aaliou3lem9  23909  1cubr  24369  dchrvmasumlema  24989  selbergsb  25064  ostth  25128  istrkg2ld  25159  tglowdim1i  25196  tgdim01  25202  legtrid  25286  midex  25429  ishpg  25451  brbtwn2  25585  colinearalg  25590  ax5seg  25618  axpasch  25621  axlowdimlem6  25627  axeuclidlem  25642  axeuclid  25643  usgra2edg1  25912  nbgraop1  25954  nbgraf1olem1  25970  el2wlkonot  26396  el2spthonot  26397  el2wlkonotot0  26399  4cycl2vnunb  26544  vdn0frgrav2  26550  vdgn0frgrav2  26551  usg2spot2nb  26592  usgreg2spot  26594  lpni  26722  nmobndseqi  27018  hhcmpl  27441  shne0i  27691  nmcopexi  28270  nmcfnexi  28294  cdj3lem3b  28683  rexcom4f  28701  iunin1f  28757  disjunsn  28789  ofpreima  28848  fpwrelmapffslem  28895  tosglblem  29000  xrnarchi  29069  ordtconlem1  29298  lmdvg  29327  esumfsup  29459  bnj168  30052  bnj1185  30118  bnj1542  30181  bnj865  30247  bnj916  30257  bnj983  30275  bnj1176  30327  bnj1189  30331  bnj1296  30343  bnj1398  30356  bnj1450  30372  bnj1463  30377  cvmliftlem15  30534  cvmlift2lem12  30550  dffr5  30896  dfon2lem9  30940  soseq  30995  noseponlem  31065  nosepon  31066  nodenselem4  31083  nodenselem5  31084  nofulllem5  31105  brbigcup  31175  elfuns  31192  brimage  31203  brimg  31214  dfrecs2  31227  imagesset  31230  brub  31231  brsegle  31385  gtinfOLD  31484  filnetlem4  31546  bj-rexcom4a  32064  bj-rexcom4bv  32065  bj-rexcom4b  32066  bj-elsngl  32149  bj-rest10  32222  bj-restreg  32233  bj-mpt2mptALT  32253  iundif1  32553  matunitlindflem1  32575  poimirlem1  32580  poimirlem30  32609  poimirlem32  32611  poimir  32612  ismblfin  32620  volsupnfl  32624  itg2addnclem3  32633  fdc  32711  isfldidl  33037  prtlem10  33168  prter2  33184  islshpat  33322  lshpsmreu  33414  2dim  33774  islpln5  33839  lplnexatN  33867  islvol5  33883  dalem18  33985  dalem20  33997  lhpexle2  34314  lhpexle3  34316  lhpex2leN  34317  4atex2  34381  4atex2-0bOLDN  34383  cdlemftr3  34871  cdlemg17pq  34978  cdlemg19  34990  cdlemg21  34992  cdlemg33d  35015  dva1dim  35291  dih1dimatlem  35636  dihglb2  35649  dvh2dim  35752  mapdrvallem2  35952  mapdpglem3  35982  hdmapglem7a  36237  elrfirn  36276  isnacs2  36287  isnacs3  36291  sbc2rex  36369  4rexfrabdioph  36380  eldioph4b  36393  fphpd  36398  fiphp3d  36401  rencldnfilem  36402  rmxdioph  36601  expdiophlem1  36606  islnm2  36666  elimaint  36959  cnviun  36961  imaiun1  36962  coiun1  36963  elintima  36964  briunov2  36993  clsk3nimkb  37358  prmunb2  37532  zfregs2VD  38098  evth2f  38197  evthf  38209  ndisj2  38243  fnlimabslt  38746  stoweidlem28  38921  fourierdlem63  39062  fourierdlem65  39064  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem100  39099  sge0pnfmpt  39338  ovn0  39456  smfaddlem1  39649  smflimlem4  39660  2rexsb  39819  2rexrsb  39820  cbvrex2  39822  2reu5a  39826  umgr2edg1  40438  umgr2edgneu  40441  nbgrsym  40591  isuvtxa  40621  usgr2pth0  40971  1wlkiswwlksupgr2  41074  clwwlksnun  41281  4cycl2vnunb-av  41460  fusgr2wsp2nb  41498  fusgreg2wsp  41500  copisnmnd  41599  pgrpgt2nabl  41941  islindeps  42036  lindslinindsimp1  42040  lindslinindsimp2  42046  islindeps2  42066  islininds2  42067  isldepslvec2  42068  ldepslinc  42092
 Copyright terms: Public domain W3C validator