MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exbii Unicode version

Theorem exbii 1667
Description: Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.)
Hypothesis
Ref Expression
exbii.1
Assertion
Ref Expression
exbii

Proof of Theorem exbii
StepHypRef Expression
1 exbi 1666 . 2
2 exbii.1 . 2
31, 2mpg 1620 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  E.wex 1612
This theorem is referenced by:  2exbii  1668  3exbii  1669  exanali  1670  exancom  1671  19.43  1693  sbequ8  1744  19.12vvv  1765  19.41vv  1772  19.41vvv  1773  19.41vvvv  1774  exdistr  1776  19.42vvv  1778  exdistr2  1779  3exdistr  1780  equvin  1804  excom  1849  excom13  1851  exrot4  1853  eeor  1976  19.12vv  1986  eean  1987  eeeanv  1989  ee4anv  1990  2sb5  2187  2sb5rf  2195  2sb8e  2211  sb8eu  2318  sb8euOLD  2319  eu1  2327  sbmo  2335  2moswap  2369  2eu1OLD  2377  exists1  2388  clelabOLD  2602  clabel  2603  sbabel  2650  sbabelOLD  2651  nabbi  2790  nabbiOLD  2791  rexbii2  2957  r2exlem  2977  r2exfOLD  2979  r19.41v  3009  r19.41  3010  isset  3113  rexv  3124  ceqsex2  3147  ceqsex3v  3149  gencbvex  3153  vtocl2  3162  vtocl3  3163  spc3gv  3199  ceqsrexv  3233  rexab  3262  rexrab2  3267  euxfr  3285  euind  3286  reu6  3288  reu3  3289  2reuswap  3302  reuind  3303  2reu5lem3  3307  2reu5  3308  sbccomlem  3406  rmo2  3427  rexun  3683  reupick3  3782  abn0  3804  pssnel  3893  rexsns  4062  rexsnsOLD  4063  exsnrex  4067  snprc  4093  euabsn2  4101  reusn  4103  eusn  4106  elunirab  4261  unipr  4262  uniun  4268  uniin  4269  uni0b  4274  uniintsn  4324  iuncom4  4338  dfiun2g  4362  iunn0  4390  iunxiun  4413  disjor  4436  cbvopab2  4523  cbvopab2v  4526  unopab  4527  axrep1  4564  axrep4  4567  axrep5  4568  zfrep4  4571  axsep  4572  zfnuleu  4578  axnulALT  4579  0ex  4582  vprc  4590  inex1  4593  inuni  4614  axpweq  4629  zfpow  4631  axpow2  4632  axpow3  4633  pwex  4635  reusv5OLD  4662  zfpair  4689  zfpair2  4692  eqvinop  4736  copsexg  4737  copsexgOLD  4738  opabn0  4783  iunopab  4788  dfid3  4801  elxp2  5022  opeliunxp  5056  xpiundi  5059  xpiundir  5060  elvvv  5064  csbxp  5086  eliunxp  5145  exopxfr  5151  relop  5158  opelco2g  5175  cnvco  5193  cnvuni  5194  dfdm3  5195  dfrn2  5196  dfrn3  5197  elrng  5199  dfdm4  5200  csbdm  5202  eldm2g  5204  dmun  5214  dmin  5215  dmiun  5216  dmuni  5217  dmopab  5218  dmi  5222  elrn  5248  rnopab  5252  dmcosseq  5269  dmres  5299  elres  5314  elsnres  5315  dfima2  5344  elima3  5349  imadmrn  5352  imai  5354  args  5370  rniun  5421  xpdifid  5440  ssrnres  5450  dmsnn0  5478  dmsnopg  5484  cnvresima  5501  mptpreima  5505  dfco2  5511  coundi  5513  coundir  5514  resco  5516  imaco  5517  rnco  5518  coiun  5522  coi1  5528  coass  5531  xpco  5552  dffun2  5603  dffun5  5606  imadif  5668  funimaexg  5670  brprcneu  5864  dffv2  5946  fndmin  5994  fvn0ssdmfun  6022  abrexco  6156  imaiun  6157  isomin  6233  dfoprab2  6343  cbvoprab2  6370  zfun  6593  uniex2  6595  uniuni  6609  elxp4  6744  elxp5  6745  fun11iun  6760  f11o  6762  fvresex  6773  opabex3d  6778  opabex3  6779  abexssex  6782  abexex  6783  oprabrexex2  6790  releldm2  6850  dfopab2  6854  dfoprab3s  6855  fsplit  6905  frxp  6910  suppvalbr  6922  cnvimadfsn  6927  brtpos2  6980  oarec  7230  oeeu  7271  domen  7549  mapsnen  7613  xpsnen  7621  xpcomco  7627  xpassen  7631  inf2  8061  zfinf  8077  axinf2  8078  zfinf2  8080  rankuni  8302  scott0  8325  cp  8330  ween  8437  aceq1  8519  aceq0  8520  aceq2  8521  dfac5lem1  8525  dfac5lem2  8526  dfac5lem3  8527  kmlem3  8553  kmlem14  8564  kmlem15  8565  kmlem16  8566  cflem  8647  cf0  8652  cfval2  8661  cfss  8666  cfslb  8667  fin23lem32  8745  axdc2lem  8849  zfac  8861  ac9  8884  ac9s  8894  axpowndlem3  8996  axpowndlem3OLD  8997  zfcndrep  9013  zfcndun  9014  zfcndpow  9015  zfcndinf  9017  zfcndac  9018  axgroth5  9223  axgroth2  9224  grothpw  9225  axgroth6  9227  axgroth3  9230  axgroth4  9231  grothprim  9233  grothtsk  9234  genpass  9408  ltexprlem1  9435  ltexprlem4  9438  supmul1  10533  supmullem2  10535  2rexuz  11162  nnwos  11178  hashfun  12495  wwlktovfo  12896  cbvsum  13517  cbvprod  13722  iprodmul  13796  maxprmfct  14254  4sqlem12  14474  vdwmc  14496  cshwrepswhash1  14587  imasleval  14938  isacs2  15050  gsumval3eu  16907  lidlnz  17876  isbasis2g  19449  tgval2  19457  ntreq0  19578  lmff  19802  cmpfi  19908  is1stc2  19943  1stcelcls  19962  unisngl  20028  isfbas2  20336  elfg  20372  alexsubALTlem3  20549  ustfilxp  20715  metrest  21027  metuel2  21082  restmetu  21090  cmetss  21753  dchrvmasumlema  23685  istrkg2ld  23858  usgraedg4  24387  3v3e3cycl2  24664  wlknwwlknsur  24712  wlkiswwlksur  24719  wwlkextsur  24731  el2wlkonot  24869  el2spthonot  24870  el2wlkonotot0  24872  frgrawopreglem2  25045  usg2spot2nb  25065  isgrpo  25198  ismgmOLD  25322  nmo  27384  2reuswap2  27387  rexunirn  27390  disjorf  27440  fcoinvbr  27461  mpt2mptxf  27518  cnvoprab  27546  fpwrelmapffslem  27555  ordtconlem1  27906  ddemeas  28208  eulerpartlemgvv  28315  axextprim  29073  axrepprim  29074  axunprim  29075  axpowprim  29076  axregprim  29077  axinfprim  29078  axacprim  29079  dftr6  29179  coep  29180  coepr  29181  dffr5  29182  dfpo2  29184  cnvco1  29189  cnvco2  29190  eldm3  29191  fundmpss  29196  dfdm5  29206  dfrn5  29207  elima4  29209  domep  29225  axextdfeq  29230  19.12b  29234  axextndbi  29237  wfrlem11  29353  frrlem5c  29393  nofulllem5  29466  brtxp  29530  brpprod  29535  brsset  29539  dfon3  29542  brtxpsd  29544  elfix  29553  dffix2  29555  sscoid  29563  dffun10  29564  elfuns  29565  elsingles  29568  snelsingles  29572  dfiota3  29573  brimg  29587  brapply  29588  brcup  29589  brcap  29590  brsuccf  29591  funpartlem  29592  brrestrict  29599  dfrdg4  29600  tfrqfree  29601  supaddc  30041  supadd  30042  ismblfin  30055  itg2addnclem3  30068  itg2addnc  30069  neifg  30189  sbcexfi  30520  sbccom2lem  30529  prtlem16  30610  prter2  30622  diophrex  30709  19.36vv  31288  19.37vv  31290  pm11.58  31296  pm11.6  31298  pm13.192  31317  2sbc5g  31323  iotasbc2  31327  rfcnnnub  31411  stoweidlem34  31816  stoweidlem35  31817  stoweidlem60  31842  rmoanim  32184  2rmoswap  32189  euelss  32553  cicsym  32588  opeliun2xp  32922  eliunxp2  32923  eximp-surprise  33199  onfrALTlem5  33314  onfrALTlem1  33320  ax6e2nd  33331  2sb5nd  33333  en3lplem2VD  33644  relopabVD  33701  ax6e2ndVD  33708  2sb5ndVD  33710  ax6e2ndALT  33730  2sb5ndALT  33732  bnj89  33774  bnj133  33780  bnj1019  33838  bnj1101  33843  bnj1109  33845  bnj1143  33849  bnj1198  33854  bnj1304  33878  bnj605  33965  bnj607  33974  bnj600  33977  bnj865  33981  bnj916  33991  bnj983  34009  bnj985  34011  bnj996  34013  bnj1033  34025  bnj1083  34034  bnj1090  34035  bnj1093  34036  bnj1110  34038  bnj1128  34046  bnj1145  34049  bnj1171  34056  bnj1172  34057  bnj1174  34059  bnj1176  34061  bnj1186  34063  bnj1189  34065  bnj1253  34073  bnj1279  34074  bnj1371  34085  bnj1374  34087  bnj1312  34114  bj-eeanvw  34267  bj-clabel  34369  bj-axrep1  34374  bj-axrep4  34377  bj-axrep5  34378  bj-axsep  34379  bj-zfpow  34381  bj-denotes  34434  bj-rexvwv  34442  bj-rexcom4  34445  bj-csbsnlem  34470  bj-snsetex  34521  bj-elsngl  34526  bj-snglc  34527  bj-nul  34585  islshpat  34742  islpln5  35259  islvol5  35303  pmapglb  35494  polval2N  35630  cdlemftr3  36291  dibelval3  36874  dicelval3  36907  dihglb2  37069  rp-isfinite6  37744  xpcogend  37773  ndisj  37793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185  df-ex 1613
  Copyright terms: Public domain W3C validator