Theorem exbii 1582

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	⊢ (∃xφ ↔ ∃xψ)

Proof of Theorem exbii

Step	Hyp	Ref	Expression
1		exbi 1581	. 2 ⊢ (∀x(φ ↔ ψ) → (∃xφ ↔ ∃xψ))
2		exbii.1	. 2 ⊢ (φ ↔ ψ)
3	1, 2	mpg 1548	1 ⊢ (∃xφ ↔ ∃xψ)

Syntax hints:   ↔ wb 176  ∃wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557

This theorem depends on definitions:  df-bi 177  df-ex 1542

This theorem is referenced by:  2exbii  1583  3exbii  1584  exanali  1585  exancom  1586  19.43  1605  exiftruOLD  1658  excom  1741  excom13  1743  exrot4  1745  eeor  1885  19.12vv  1898  19.41vv  1902  19.41vvv  1903  19.41vvvv  1904  exdistr  1906  19.42vvv  1908  exdistr2  1909  3exdistr  1910  4exdistr  1911  eean  1912  eeeanv  1914  ee4anv  1915  equsex  1962  2sb5  2112  2sb5rf  2117  sbel2x  2125  exsbOLD  2131  2exsb  2132  sb8eu  2222  eu1  2225  eu2  2229  sbmo  2234  moanim  2260  2moswap  2279  2eu1  2284  exists1  2293  clelab  2473  clabel  2474  sbabel  2515  rexbii2  2643  r2exf  2650  r19.41  2763  isset  2863  rexv  2873  ceqsex2  2895  ceqsex3v  2897  gencbvex  2901  vtocl2  2910  vtocl3  2911  spc3gv  2944  ceqsrexv  2972  rexab  2999  rexrab2  3004  euxfr  3022  euind  3023  reu6  3025  reu3  3026  2reuswap  3038  reuind  3039  2reu5lem3  3043  2reu5  3044  sbccomlem  3116  rmo2  3131  rexun  3443  reupick3  3540  abn0  3568  pssnel  3615  rexsns  3764  snprc  3788  euabsn2  3791  reusn  3793  eusn  3796  elunirab  3904  unipr  3905  uniun  3910  uniin  3911  uni0b  3916  uniintsn  3963  iuncom4  3976  dfiun2g  3999  iunn0  4026  iunxiun  4048  axxpprim  4090  axcnvprim  4091  axssetprim  4092  axsiprim  4093  axtyplowerprim  4094  axins2prim  4095  axins3prim  4096  ninexg  4097  snex  4111  1cex  4142  elpw1  4144  elpw12  4145  elpw11c  4147  elpw121c  4148  elpw131c  4149  elpw141c  4150  elpw151c  4151  elpw161c  4152  elpw171c  4153  elpw181c  4154  elpw191c  4155  elpw1101c  4156  elpw1111c  4157  eluni1g  4172  otkelins2kg  4253  otkelins3kg  4254  opkelcokg  4261  opkelimagekg  4271  imacok  4282  xpkvexg  4285  dfimak2  4298  dfpw12  4301  insklem  4304  ndisjrelk  4323  unipw1  4325  dfpw2  4327  dfeu2  4333  dfaddc2  4381  dfnnc2  4395  elsuc  4413  addcass  4415  nnsucelrlem1  4424  preaddccan2lem1  4454  ltfinex  4464  ssfin  4470  eqpwrelk  4478  eqpw1relk  4479  ncfinraiselem2  4480  ncfinlowerlem1  4482  eqtfinrelk  4486  evenfinex  4503  oddfinex  4504  evenodddisjlem1  4515  nnadjoinlem1  4519  nnpweqlem1  4522  srelk  4524  sfintfinlem1  4531  tfinnnlem1  4533  spfinex  4537  vfinspsslem1  4550  vfinspss  4551  vfinncsp  4554  dfop2lem1  4573  eqvinop  4606  copsexg  4607  opeq  4619  cbvopab2  4633  cbvopab2v  4636  unopab  4638  opabn0  4716  el1st  4729  setconslem1  4731  setconslem2  4732  setconslem3  4733  setconslem4  4734  setconslem6  4736  setconslem7  4737  df1st2  4738  dfswap2  4741  dfco1  4748  dfid3  4768  elxp2  4802  xpiundi  4817  xpiundir  4818  opeliunxp  4820  eliunxp  4821  cnvco  4894  cnvuni  4895  elrn2  4897  eldm  4898  eldm2  4899  dfrn3  4903  dfrn4  4904  dmun  4912  dmin  4913  dmuni  4914  dmopab  4915  dmi  4919  elimapw1  4944  elimapw12  4945  elimapw13  4946  elimapw11c  4948  dfima3  4951  rnopab  4967  dmcoss  4971  dmcosseq  4973  dmres  4986  elsnres  4996  imadmrn  5008  imai  5010  rnuni  5038  ssrnres  5059  dmsnn0  5064  dmsnopg  5066  rnsnop  5075  cnvresima  5077  dfco2  5080  coundi  5082  coundir  5083  resco  5085  imaco  5086  rnco  5087  coiun  5090  coi1  5094  coass  5097  dfcnv2  5100  elxp4  5108  df2nd2  5111  dffun2  5119  dffun5  5122  nfunv  5138  imadif  5171  iunfopab  5204  fun11iun  5305  f11o  5315  dmfco  5381  abrexco  5463  imaiun  5464  funiunfv  5467  isomin  5496  opbr1st  5501  opbr2nd  5502  dfdm4  5507  dfrn5  5508  dmsi  5519  dfoprab2  5558  cbvoprab2  5568  mptpreima  5682  brsnsi1  5775  brsnsi2  5776  brco1st  5777  brco2nd  5778  trtxp  5781  elfix  5787  brimage  5793  oqelins4  5794  dmtxp  5802  txpcofun  5803  otsnelsi3  5805  releqel  5807  releqmpt2  5809  composeex  5820  disjex  5823  addcfnex  5824  funsex  5828  qrpprod  5836  brpprod  5839  dmpprod  5840  crossex  5850  pw1fnex  5852  pw1fnf1o  5855  fnfullfunlem1  5856  fvfullfunlem1  5861  domfnex  5870  ranfnex  5871  clos1ex  5876  transex  5910  refex  5911  antisymex  5912  connexex  5913  foundex  5914  extex  5915  symex  5916  frds  5935  ecdmn0  5967  qsexg  5982  enex  6031  xpassenlem  6056  xpassen  6057  enpw1lem1  6061  enmap2lem1  6063  enmap1lem1  6069  enpw1pw  6075  enprmaplem1  6076  nenpw1pwlem1  6084  lecex  6115  elncs  6119  ovmuc  6130  mucex  6133  ovcelem1  6171  ceexlem1  6173  ceex  6174  ce0nnul  6177  ce0addcnnul  6179  el2c  6191  taddc  6229  tcfnex  6244  csucex  6259  nnltp1clem1  6261  addccan2nclem1  6263  addccan2nclem2  6264  nmembers1lem1  6268  nncdiv3lem1  6275  nncdiv3lem2  6276  nnc3n3p1  6278  spacvallem1  6281  nchoicelem10  6298  nchoicelem11  6299  nchoicelem16  6304  dmfrec  6316  fnfreclem1  6317