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

Theorem rexbii 3244
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 3242 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wcel 2105  wrex 3136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-rex 3141
This theorem is referenced by:  2rexbii  3245  2ex2rexrot  3247  rexcom4a  3248  r19.29rOLD  3253  r19.29imd  3254  rexnal2  3255  ralnex3OLD  3260  r19.41vv  3346  r19.42v  3347  r19.43  3348  rexcom  3352  rexcom13  3357  rexrot4  3359  3reeanv  3366  2ralor  3367  cbvrex2vw  3460  cbvrex2v  3463  rexcom4b  3522  rexcom4OLD  3524  ceqsrex2v  3648  clel5  3654  reu7  3720  2reu5a  3732  0el  4317  n0snor2el  4756  uni0b  4855  iuncom  4917  iuncom4  4918  iuniin  4922  dfiunv2  4951  iunab  4966  iunn0  4980  iunin2  4984  iundif2  4987  iunun  5006  iunxiun  5010  iunpwss  5020  axrep6  5188  inuni  5237  reusv2lem5  5293  iunopab  5437  dffr2  5513  frc  5514  frminex  5528  dfepfr  5533  epfrc  5534  xpiundi  5615  xpiundir  5616  reliin  5683  iunxpf  5712  cnvuni  5750  dmiun  5775  dmopab2rex  5779  elres  5884  elidinxp  5904  dfima3  5925  dffr3  5955  rniun  5999  xpdifid  6018  dminxp  6030  imaco  6097  coiun  6102  dffr4  6157  tz6.26  6172  sucel  6257  isarep1  6435  rexrn  6845  ralrn  6846  elrnrexdmb  6848  fnasrn  6899  rexima  6990  ralima  6991  abrexco  6994  imaiun  6995  fliftcnv  7053  rexrnmpo  7279  iunpw  7482  abrexex2g  7654  el2xptp  7724  rdglem1  8040  tz7.49  8070  oarec  8177  omeu  8200  qsid  8352  eroveu  8381  ixp0  8483  fimax2g  8752  marypha2lem2  8888  dfsup2  8896  infcllem  8939  dfoi  8963  wemapsolem  9002  zfregcl  9046  zfreg  9047  zfregfr  9056  oemapso  9133  zfregs2  9163  infenaleph  9505  isinfcard  9506  kmlem7  9570  kmlem13  9576  fin23lem26  9735  dffin1-5  9798  fin12  9823  numth  9882  ac6n  9895  zorn2lem7  9912  zorng  9914  brdom7disj  9941  brdom6disj  9942  uniwun  10150  axgroth5  10234  axgroth4  10242  grothprim  10244  npomex  10406  genpass  10419  elreal  10541  dfinfre  11610  infrenegsup  11612  uzwo  12299  ublbneg  12321  xrinfmss2  12692  4fvwrd4  13015  fsuppmapnn0fiubex  13348  fsuppmapnn0ub  13351  mptnn0fsuppr  13355  hashge2el2dif  13826  dfrtrclrec2  14404  rexanuz  14693  rexfiuz  14695  clim0  14851  cbvsum  15040  incexc2  15181  cbvprod  15257  fprodle  15338  iprodmul  15345  divalglem10  15741  divalgb  15743  ncoprmlnprm  16056  pythagtriplem2  16142  pythagtriplem19  16158  pythagtrip  16159  pceu  16171  prmreclem6  16245  4sqlem12  16280  cshwshashlem1  16417  cshwshash  16426  imasaddfnlem  16789  isdrs2  17537  pmtrprfvalrn  18545  pgpfac1lem5  19130  dvdsrval  19324  opprunit  19340  lsmspsn  19785  lsmelval2  19786  islpidl  19947  mat1dimelbas  21008  mat1dimbas  21009  mdetunilem8  21156  pmatcollpw2lem  21313  tgval2  21492  ntreq0  21613  isclo2  21624  neiptopnei  21668  ist0-3  21881  tgcmp  21937  cmpfi  21944  is1stc2  21978  unisngl  22063  xkobval  22122  txtube  22176  txcmplem1  22177  xkococnlem  22195  eltsms  22668  metrest  23061  iscau3  23808  bcth  23859  pmltpc  23978  itg2i1fseq  24283  itg2cn  24291  plyun0  24714  aaliou3lem9  24866  1cubr  25347  dchrvmasumlema  26003  selbergsb  26078  ostth  26142  istrkg2ld  26173  tglowdim1i  26214  legtrid  26304  midex  26450  ishpg  26472  brbtwn2  26618  colinearalg  26623  ax5seg  26651  axpasch  26654  axlowdimlem6  26660  axeuclidlem  26675  axeuclid  26676  elntg2  26698  umgr2edg1  26920  umgr2edgneu  26923  nbgrsym  27072  isuvtx  27104  usgr2pth0  27473  wlkiswwlksupgr2  27582  clwwlknun  27818  4cycl2vnunb  27996  fusgreg2wsp  28042  lpni  28184  nmobndseqi  28483  hhcmpl  28904  shne0i  29152  nmcopexi  29731  nmcfnexi  29755  cdj3lem3b  30144  rexcom4f  30161  reuxfrdf  30182  iunin1f  30237  ofpreima  30338  fpwrelmapffslem  30394  tosglblem  30583  xrnarchi  30740  ordtconnlem1  31066  lmdvg  31095  esumfsup  31228  reprsuc  31785  reprdifc  31797  bnj168  31899  bnj1185  31964  bnj1542  32028  bnj865  32094  bnj916  32104  bnj983  32122  bnj1176  32174  bnj1189  32178  bnj1296  32190  bnj1398  32203  bnj1450  32219  bnj1463  32224  loop1cycl  32281  cvmliftlem15  32442  cvmlift2lem12  32458  satfvsuclem2  32504  satfvsucsuc  32509  satfdm  32513  satf0  32516  dmopab3rexdif  32549  dffr5  32886  imaindm  32919  dfon2lem9  32933  frpomin2  32976  soseq  32993  frrlem9  33028  noseponlem  33068  nosepon  33069  nolt02o  33096  brbigcup  33256  elfuns  33273  brimage  33284  brimg  33295  dfrecs2  33308  imagesset  33311  brub  33312  brsegle  33466  filnetlem4  33626  bj-rexcom4bv  34095  bj-rexcom4b  34096  bj-elsngl  34177  bj-rest10  34273  bj-restreg  34284  bj-mpomptALT  34303  nlpineqsn  34571  fvineqsneq  34575  iundif1  34747  matunitlindflem1  34769  poimirlem1  34774  poimirlem30  34803  poimirlem32  34805  poimir  34806  ismblfin  34814  volsupnfl  34818  itg2addnclem3  34826  fdc  34901  isfldidl  35227  eldmqsres2  35425  n0elqs  35464  rnxrncnvepres  35528  rnxrnidres  35529  dfcoels  35555  br1cossinres  35567  br1cossinidres  35569  br1cossincnvepres  35570  br1cossxrnidres  35571  br1cossxrncnvepres  35572  br1cossxrncnvssrres  35628  eldmqs1cossres  35773  prtlem10  35881  prter2  35897  islshpat  36033  lshpsmreu  36125  2dim  36486  islpln5  36551  lplnexatN  36579  islvol5  36595  dalem18  36697  dalem20  36709  lhpexle2  37026  lhpexle3  37028  lhpex2leN  37029  4atex2  37093  4atex2-0bOLDN  37095  cdlemftr3  37581  cdlemg17pq  37688  cdlemg19  37700  cdlemg21  37702  cdlemg33d  37725  dva1dim  38001  dih1dimatlem  38345  dihglb2  38358  dvh2dim  38461  mapdrvallem2  38661  mapdpglem3  38691  hdmapglem7a  38943  iunsn  38996  dffltz  39149  elrfirn  39170  isnacs2  39181  isnacs3  39185  sbc2rex  39262  4rexfrabdioph  39273  eldioph4b  39286  fphpd  39291  fiphp3d  39294  rencldnfilem  39295  rmxdioph  39491  expdiophlem1  39496  islnm2  39556  elimaint  39871  cnviun  39873  imaiun1  39874  coiun1  39875  elintima  39876  briunov2  39905  clsk3nimkb  40268  expandrexn  40504  prmunb2  40520  zfregs2VD  41052  evth2f  41149  evthf  41161  ndisj2  41190  fnlimabslt  41836  climbddf  41844  limsupub  41861  limsuppnflem  41867  limsupubuz  41870  limsupre2lem  41881  limsupreuz  41894  limsupvaluz2  41895  cnrefiisplem  41986  cnrefiisp  41987  stoweidlem28  42190  fourierdlem63  42331  fourierdlem65  42333  fourierdlem89  42357  fourierdlem90  42358  fourierdlem91  42359  fourierdlem100  42368  sge0pnfmpt  42604  ovn0  42725  smfaddlem1  42916  smflimlem4  42927  2rexsb  43176  2rexrsb  43177  cbvrex2  43179  2reu8i  43189  copisnmnd  43953  smndex1mgm  44007  smndex1n0mnd  44012  pgrpgt2nabl  44342  islindeps  44436  lindslinindsimp1  44440  lindslinindsimp2  44446  islindeps2  44466  islininds2  44467  isldepslvec2  44468  ldepslinc  44492
  Copyright terms: Public domain W3C validator