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

Theorem rexbii 3251
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 622 . 2 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32rexbii2 3249 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wcel 2106  wrex 3143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-rex 3148
This theorem is referenced by:  2rexbii  3252  2ex2rexrot  3254  rexcom4a  3255  r19.29rOLD  3260  r19.29imd  3261  rexnal2  3262  ralnex3OLD  3267  r19.41vv  3353  r19.42v  3354  r19.43  3355  rexcom  3359  rexcom13  3364  rexrot4  3366  3reeanv  3373  2ralor  3374  cbvrex2vw  3467  cbvrex2v  3470  rexcom4b  3529  rexcom4OLD  3531  ceqsrex2v  3654  clel5  3660  reu7  3726  2reu5a  3738  0el  4323  n0snor2el  4762  uni0b  4861  iuncom  4923  iuncom4  4924  iuniin  4927  dfiunv2  4956  iunab  4971  iunn0  4985  iunin2  4989  iundif2  4992  iunun  5011  iunxiun  5015  iunpwss  5025  axrep6  5193  inuni  5242  reusv2lem5  5298  iunopab  5442  dffr2  5518  frc  5519  frminex  5533  dfepfr  5538  epfrc  5539  xpiundi  5620  xpiundir  5621  reliin  5688  iunxpf  5717  cnvuni  5755  dmiun  5780  dmopab2rex  5784  elres  5889  elidinxp  5909  dfima3  5929  dffr3  5959  rniun  6003  xpdifid  6022  dminxp  6034  imaco  6101  coiun  6106  dffr4  6161  tz6.26  6176  sucel  6261  isarep1  6438  rexrn  6848  ralrn  6849  elrnrexdmb  6851  fnasrn  6902  rexima  6996  ralima  6997  abrexco  7000  imaiun  7001  fliftcnv  7059  rexrnmpo  7283  iunpw  7484  abrexex2g  7659  el2xptp  7729  rdglem1  8045  tz7.49  8075  oarec  8181  omeu  8204  qsid  8356  eroveu  8385  ixp0  8487  fimax2g  8756  marypha2lem2  8892  dfsup2  8900  infcllem  8943  dfoi  8967  wemapsolem  9006  zfregcl  9050  zfreg  9051  zfregfr  9060  oemapso  9137  zfregs2  9167  infenaleph  9509  isinfcard  9510  kmlem7  9574  kmlem13  9580  fin23lem26  9739  dffin1-5  9802  fin12  9827  numth  9886  ac6n  9899  zorn2lem7  9916  zorng  9918  brdom7disj  9945  brdom6disj  9946  uniwun  10154  axgroth5  10238  axgroth4  10246  grothprim  10248  npomex  10410  genpass  10423  elreal  10545  dfinfre  11614  infrenegsup  11616  uzwo  12303  ublbneg  12325  xrinfmss2  12697  4fvwrd4  13020  fsuppmapnn0fiubex  13353  fsuppmapnn0ub  13356  mptnn0fsuppr  13360  hashge2el2dif  13831  dfrtrclrec2  14409  rexanuz  14698  rexfiuz  14700  clim0  14856  cbvsum  15044  incexc2  15185  cbvprod  15261  fprodle  15342  iprodmul  15349  divalglem10  15745  divalgb  15747  ncoprmlnprm  16060  pythagtriplem2  16146  pythagtriplem19  16162  pythagtrip  16163  pceu  16175  prmreclem6  16249  4sqlem12  16284  cshwshashlem1  16421  cshwshash  16430  imasaddfnlem  16793  isdrs2  17541  pmtrprfvalrn  18538  pgpfac1lem5  19123  dvdsrval  19317  opprunit  19333  lsmspsn  19778  lsmelval2  19779  islpidl  19940  mat1dimelbas  20996  mat1dimbas  20997  mdetunilem8  21144  pmatcollpw2lem  21301  tgval2  21480  ntreq0  21601  isclo2  21612  neiptopnei  21656  ist0-3  21869  tgcmp  21925  cmpfi  21932  is1stc2  21966  unisngl  22051  xkobval  22110  txtube  22164  txcmplem1  22165  xkococnlem  22183  eltsms  22656  metrest  23049  iscau3  23796  bcth  23847  pmltpc  23966  itg2i1fseq  24271  itg2cn  24279  plyun0  24702  aaliou3lem9  24854  1cubr  25333  dchrvmasumlema  25990  selbergsb  26065  ostth  26129  istrkg2ld  26160  tglowdim1i  26201  legtrid  26291  midex  26437  ishpg  26459  brbtwn2  26606  colinearalg  26611  ax5seg  26639  axpasch  26642  axlowdimlem6  26648  axeuclidlem  26663  axeuclid  26664  elntg2  26686  umgr2edg1  26908  umgr2edgneu  26911  nbgrsym  27060  isuvtx  27092  usgr2pth0  27461  wlkiswwlksupgr2  27570  clwwlknun  27806  4cycl2vnunb  27984  fusgreg2wsp  28030  lpni  28172  nmobndseqi  28471  hhcmpl  28892  shne0i  29140  nmcopexi  29719  nmcfnexi  29743  cdj3lem3b  30132  rexcom4f  30149  reuxfrdf  30170  iunin1f  30225  ofpreima  30326  fpwrelmapffslem  30382  tosglblem  30571  xrnarchi  30728  ordtconnlem1  31054  lmdvg  31083  esumfsup  31216  reprsuc  31773  reprdifc  31785  bnj168  31887  bnj1185  31952  bnj1542  32016  bnj865  32082  bnj916  32092  bnj983  32110  bnj1176  32162  bnj1189  32166  bnj1296  32178  bnj1398  32191  bnj1450  32207  bnj1463  32212  loop1cycl  32269  cvmliftlem15  32430  cvmlift2lem12  32446  satfvsuclem2  32492  satfvsucsuc  32497  satfdm  32501  satf0  32504  dmopab3rexdif  32537  dffr5  32874  imaindm  32907  dfon2lem9  32921  frpomin2  32964  soseq  32981  frrlem9  33016  noseponlem  33056  nosepon  33057  nolt02o  33084  brbigcup  33244  elfuns  33261  brimage  33272  brimg  33283  dfrecs2  33296  imagesset  33299  brub  33300  brsegle  33454  filnetlem4  33614  bj-rexcom4bv  34083  bj-rexcom4b  34084  bj-elsngl  34165  bj-rest10  34261  bj-restreg  34272  bj-mpomptALT  34291  nlpineqsn  34559  fvineqsneq  34563  iundif1  34734  matunitlindflem1  34756  poimirlem1  34761  poimirlem30  34790  poimirlem32  34792  poimir  34793  ismblfin  34801  volsupnfl  34805  itg2addnclem3  34813  fdc  34889  isfldidl  35215  eldmqsres2  35413  n0elqs  35452  rnxrncnvepres  35516  rnxrnidres  35517  dfcoels  35543  br1cossinres  35555  br1cossinidres  35557  br1cossincnvepres  35558  br1cossxrnidres  35559  br1cossxrncnvepres  35560  br1cossxrncnvssrres  35616  eldmqs1cossres  35761  prtlem10  35869  prter2  35885  islshpat  36021  lshpsmreu  36113  2dim  36474  islpln5  36539  lplnexatN  36567  islvol5  36583  dalem18  36685  dalem20  36697  lhpexle2  37014  lhpexle3  37016  lhpex2leN  37017  4atex2  37081  4atex2-0bOLDN  37083  cdlemftr3  37569  cdlemg17pq  37676  cdlemg19  37688  cdlemg21  37690  cdlemg33d  37713  dva1dim  37989  dih1dimatlem  38333  dihglb2  38346  dvh2dim  38449  mapdrvallem2  38649  mapdpglem3  38679  hdmapglem7a  38931  iunsn  38984  dffltz  39133  elrfirn  39154  isnacs2  39165  isnacs3  39169  sbc2rex  39246  4rexfrabdioph  39257  eldioph4b  39270  fphpd  39275  fiphp3d  39278  rencldnfilem  39279  rmxdioph  39475  expdiophlem1  39480  islnm2  39540  elimaint  39855  cnviun  39857  imaiun1  39858  coiun1  39859  elintima  39860  briunov2  39889  clsk3nimkb  40252  expandrexn  40489  prmunb2  40505  zfregs2VD  41037  evth2f  41134  evthf  41146  ndisj2  41175  fnlimabslt  41822  climbddf  41830  limsupub  41847  limsuppnflem  41853  limsupubuz  41856  limsupre2lem  41867  limsupreuz  41880  limsupvaluz2  41881  cnrefiisplem  41972  cnrefiisp  41973  stoweidlem28  42176  fourierdlem63  42317  fourierdlem65  42319  fourierdlem89  42343  fourierdlem90  42344  fourierdlem91  42345  fourierdlem100  42354  sge0pnfmpt  42590  ovn0  42711  smfaddlem1  42902  smflimlem4  42913  2rexsb  43162  2rexrsb  43163  cbvrex2  43165  2reu8i  43175  copisnmnd  43905  pgrpgt2nabl  44243  islindeps  44337  lindslinindsimp1  44341  lindslinindsimp2  44347  islindeps2  44367  islininds2  44368  isldepslvec2  44369  ldepslinc  44393
  Copyright terms: Public domain W3C validator