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

Theorem rexbii 3018
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 725 . 2 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32rexbii2 3016 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 194  wcel 1975  wrex 2892
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-rex 2897
This theorem is referenced by:  2rexbii  3019  rexnal2  3020  ralnex3  3023  r19.29r  3050  r19.29imd  3051  r19.41vv  3067  r19.42v  3068  r19.43  3069  rexcom13  3076  rexrot4  3077  3reeanv  3082  2ralor  3083  cbvrex2v  3151  rexcom4  3193  rexcom4a  3194  rexcom4b  3195  ceqsrex2v  3303  reu7  3363  0el  3890  uni0b  4389  rabasiun  4449  iuncom  4453  iuncom4  4454  iuniin  4457  dfiunv2  4482  iunab  4492  iunn0  4506  iunin2  4510  iundif2  4513  iunun  4530  iunxiun  4534  iunpwss  4541  inuni  4744  reusv2lem5  4790  reuxfrd  4810  iunopab  4922  dffr2  4989  frc  4990  frminex  5004  dfepfr  5009  epfrc  5010  xpiundi  5082  xpiundir  5083  reliin  5148  iunxpf  5176  cnvuni  5215  dmiun  5238  dfima3  5371  dffr3  5400  rniun  5444  xpdifid  5463  dminxp  5475  imaco  5539  coiun  5544  dffr4  5595  tz6.26  5610  sucel  5697  isarep1  5873  rexrn  6250  ralrn  6251  elrnrexdmb  6253  fnasrn  6298  rexima  6375  ralima  6376  abrexco  6380  imaiun  6381  fliftcnv  6435  rexrnmpt2  6648  iunpw  6843  abrexex2g  7009  abrexex2  7013  el2xptp  7075  rdglem1  7371  tz7.49  7400  oarec  7502  omeu  7525  qsid  7673  eroveu  7702  ixp0  7800  fimax2g  8064  marypha2lem2  8198  dfsup2  8206  infcllem  8249  dfoi  8272  wemapsolem  8311  zfregcl  8355  zfreg  8356  zfregclOLD  8357  zfregOLD  8358  zfreg2OLD  8359  zfregfr  8365  oemapso  8435  zfregs2  8465  infenaleph  8770  isinfcard  8771  kmlem7  8834  kmlem13  8840  fin23lem26  9003  dffin1-5  9066  fin12  9091  numth  9150  ac6n  9163  zorn2lem7  9180  zorng  9182  brdom7disj  9207  brdom6disj  9208  uniwun  9414  axgroth5  9498  axgroth4  9506  grothprim  9508  npomex  9670  genpass  9683  elreal  9804  dfinfre  10847  infrenegsup  10849  uzwo  11579  ublbneg  11601  xrinfmss2  11965  4fvwrd4  12279  fsuppmapnn0fiubex  12605  fsuppmapnn0ub  12608  mptnn0fsuppr  12612  hashge2el2dif  13063  wrdlen1  13140  dfrtrclrec2  13587  rexanuz  13875  rexfiuz  13877  clim0  14027  cbvsum  14215  incexc2  14351  cbvprod  14426  fprodle  14508  iprodmul  14515  divalglem10  14905  divalgb  14907  ncoprmlnprm  15216  phisum  15275  pythagtriplem2  15302  pythagtriplem19  15318  pythagtrip  15319  pceu  15331  prmreclem6  15405  4sqlem12  15440  cshwshashlem1  15582  cshwshash  15591  imasaddfnlem  15953  isdrs2  16704  symgmov1  17577  pmtrprfvalrn  17673  pgpfac1lem5  18243  dvdsrval  18410  opprunit  18426  lsmspsn  18847  lsmelval2  18848  islpidl  19009  mat1dimelbas  20034  mat1dimbas  20035  mdetunilem8  20182  pmatcollpw2lem  20339  tgval2  20509  ntreq0  20629  isclo2  20640  neiptopnei  20684  ist0-3  20897  tgcmp  20952  cmpfi  20959  is1stc2  20993  unisngl  21078  xkobval  21137  txtube  21191  txcmplem1  21192  xkococnlem  21210  eltsms  21684  metrest  22076  iscau3  22798  bcth  22847  pmltpc  22939  itg2i1fseq  23241  itg2cn  23249  plyun0  23670  aaliou3lem9  23822  1cubr  24282  dchrvmasumlema  24902  selbergsb  24977  ostth  25041  istrkg2ld  25072  tglowdim1i  25109  tgdim01  25115  legtrid  25200  midex  25343  ishpg  25365  brbtwn2  25499  colinearalg  25504  ax5seg  25532  axpasch  25535  axlowdimlem6  25541  axeuclidlem  25556  axeuclid  25557  usgra2edg1  25674  nbgraop1  25716  nbgraf1olem1  25732  el2wlkonot  26158  el2spthonot  26159  el2wlkonotot0  26161  4cycl2vnunb  26306  vdn0frgrav2  26312  vdgn0frgrav2  26313  usg2spot2nb  26354  usgreg2spot  26356  lpni  26484  nmobndseqi  26820  hhcmpl  27243  shne0i  27493  nmcopexi  28072  nmcfnexi  28096  cdj3lem3b  28485  rexcom4f  28503  iunin1f  28559  disjunsn  28591  ofpreima  28650  fpwrelmapffslem  28697  tosglblem  28802  xrnarchi  28871  ordtconlem1  29100  lmdvg  29129  esumfsup  29261  bnj168  29854  bnj1185  29920  bnj1542  29983  bnj865  30049  bnj916  30059  bnj983  30077  bnj1176  30129  bnj1189  30133  bnj1296  30145  bnj1398  30158  bnj1450  30174  bnj1463  30179  cvmliftlem15  30336  cvmlift2lem12  30352  dffr5  30698  dfon2lem9  30742  soseq  30797  noseponlem  30867  nosepon  30868  nodenselem4  30885  nodenselem5  30886  nofulllem5  30907  brbigcup  30977  elfuns  30994  brimage  31005  brimg  31016  dfrecs2  31029  imagesset  31032  brub  31033  brsegle  31187  gtinfOLD  31286  filnetlem4  31348  bj-rexcom4a  31863  bj-rexcom4bv  31864  bj-rexcom4b  31865  bj-elsngl  31948  bj-rest10  32021  bj-restreg  32032  bj-mpt2mptALT  32052  iundif1  32352  matunitlindflem1  32374  poimirlem1  32379  poimirlem30  32408  poimirlem32  32410  poimir  32411  ismblfin  32419  volsupnfl  32423  itg2addnclem3  32432  fdc  32510  isfldidl  32836  prtlem10  32967  prter2  32983  islshpat  33121  lshpsmreu  33213  2dim  33573  islpln5  33638  lplnexatN  33666  islvol5  33682  dalem18  33784  dalem20  33796  lhpexle2  34113  lhpexle3  34115  lhpex2leN  34116  4atex2  34180  4atex2-0bOLDN  34182  cdlemftr3  34670  cdlemg17pq  34777  cdlemg19  34789  cdlemg21  34791  cdlemg33d  34814  dva1dim  35090  dih1dimatlem  35435  dihglb2  35448  dvh2dim  35551  mapdrvallem2  35751  mapdpglem3  35781  hdmapglem7a  36036  elrfirn  36075  isnacs2  36086  isnacs3  36090  sbc2rex  36168  4rexfrabdioph  36179  eldioph4b  36192  fphpd  36197  fiphp3d  36200  rencldnfilem  36201  rmxdioph  36400  expdiophlem1  36405  islnm2  36465  elimaint  36758  cnviun  36760  imaiun1  36761  coiun1  36762  elintima  36763  briunov2  36792  clsk3nimkb  37157  prmunb2  37331  zfregs2VD  37897  evth2f  37996  evthf  38008  ndisj2  38042  fnlimabslt  38546  stoweidlem28  38721  fourierdlem63  38862  fourierdlem65  38864  fourierdlem89  38888  fourierdlem90  38889  fourierdlem91  38890  fourierdlem100  38899  sge0pnfmpt  39138  ovn0  39256  smfaddlem1  39449  smflimlem4  39460  2rexsb  39619  2rexrsb  39620  cbvrex2  39622  2reu5a  39626  n0snor2el  40119  umgr2edg1  40436  umgr2edgneu  40439  nbgrsym  40589  isuvtxa  40619  usgr2pth0  40969  1wlkiswwlksupgr2  41072  clwwlksnun  41279  4cycl2vnunb-av  41458  fusgr2wsp2nb  41496  fusgreg2wsp  41498  copisnmnd  41597  pgrpgt2nabl  41939  islindeps  42034  lindslinindsimp1  42038  lindslinindsimp2  42044  islindeps2  42064  islininds2  42065  isldepslvec2  42066  ldepslinc  42090
  Copyright terms: Public domain W3C validator