Theorem exbii 1567

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

Step	Hyp	Ref	Expression
1		exbi 1566	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
2		exbii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpg 1410	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)

Syntax hints:   ↔ wb 104  ∃wex 1451

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-ial 1497

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2exbii  1568  3exbii  1569  exancom  1570  excom13  1650  exrot4  1652  eeor  1656  sbcof2  1764  sbequ8  1801  sbidm  1805  sborv  1844  19.41vv  1857  19.41vvv  1858  19.41vvvv  1859  exdistr  1861  19.42vvv  1864  exdistr2  1866  3exdistr  1867  4exdistr  1868  eean  1881  eeeanv  1883  ee4anv  1884  2sb5  1934  2sb5rf  1940  sbel2x  1949  sbexyz  1954  sbex  1955  exsb  1959  2exsb  1960  sb8eu  1988  sb8euh  1998  eu1  2000  eu2  2019  2moswapdc  2065  2exeu  2067  exists1  2071  clelab  2239  clabel  2240  sbabel  2281  rexbii2  2420  r2exf  2427  nfrexdya  2444  r19.41  2560  r19.43  2563  isset  2663  rexv  2675  ceqsex2  2697  ceqsex3v  2699  gencbvex  2703  ceqsrexv  2785  rexab  2815  rexrab2  2820  euxfrdc  2839  euind  2840  reu6  2842  reu3  2843  2reuswapdc  2857  reuind  2858  sbccomlem  2951  rmo2ilem  2966  rexun  3222  reupick3  3327  abn0r  3353  abn0m  3354  rabn0m  3356  rexsns  3529  exsnrex  3532  snprc  3554  euabsn2  3558  reusn  3560  eusn  3563  elunirab  3715  unipr  3716  uniun  3721  uniin  3722  iuncom4  3786  dfiun2g  3811  iunn0m  3839  iunxiun  3860  disjnim  3886  cbvopab2  3962  cbvopab2v  3965  unopab  3967  zfnuleu  4012  0ex  4015  vnex  4019  inex1  4022  intexabim  4037  iinexgm  4039  inuni  4040  unidif0  4051  axpweq  4055  zfpow  4059  axpow2  4060  axpow3  4061  vpwex  4063  zfpair2  4092  mss  4108  exss  4109  opm  4116  eqvinop  4125  copsexg  4126  opabm  4162  iunopab  4163  zfun  4316  uniex2  4318  uniuni  4332  rexxfrd  4344  dtruex  4434  zfinf2  4463  elxp2  4517  opeliunxp  4554  xpiundi  4557  xpiundir  4558  elvvv  4562  eliunxp  4638  rexiunxp  4641  relop  4649  elco  4665  opelco2g  4667  cnvco  4684  cnvuni  4685  dfdm3  4686  dfrn2  4687  dfrn3  4688  elrng  4690  dfdm4  4691  eldm2g  4695  dmun  4706  dmin  4707  dmiun  4708  dmuni  4709  dmopab  4710  dmi  4714  dmmrnm  4718  elrn  4742  rnopab  4746  dmcosseq  4768  dmres  4798  elres  4813  elsnres  4814  dfima2  4841  elima3  4846  imadmrn  4849  imai  4853  args  4866  rniun  4907  ssrnres  4939  dmsnm  4962  dmsnopg  4968  elxp4  4984  elxp5  4985  cnvresima  4986  mptpreima  4990  dfco2  4996  coundi  4998  coundir  4999  resco  5001  imaco  5002  rnco  5003  coiun  5006  coi1  5012  coass  5015  xpcom  5043  dffun2  5091  imadif  5161  imainlem  5162  funimaexglem  5164  fun11iun  5344  f11o  5356  brprcneu  5368  nfvres  5408  fndmin  5481  abrexco  5614  imaiun  5615  dfoprab2  5772  cbvoprab2  5798  rexrnmpo  5840  opabex3d  5973  opabex3  5974  abexssex  5977  abexex  5978  oprabrexex2  5982  releldm2  6037  dfopab2  6041  dfoprab3s  6042  cnvoprab  6085  brtpos2  6102  tfr1onlemaccex  6199  tfrcllembxssdm  6207  tfrcllemaccex  6212  domen  6599  mapsnen  6659  xpsnen  6668  xpcomco  6673  xpassen  6677  fimax2gtri  6748  supelti  6841  subhalfnqq  7170  ltbtwnnq  7172  prnmaxl  7244  prnminu  7245  prarloc  7259  genpdflem  7263  genpassl  7280  genpassu  7281  ltexprlemm  7356  2rexuz  9279  seq3f1olemp  10168  cbvsum  11021  inffinp1  11787  unct  11797  isbasis2g  12055  tgval2  12063  ntreq0  12144  lmff  12260  metrest  12495  bj-axempty  12783  bj-axempty2  12784  bj-vprc  12786  bdinex1  12789  bj-zfpair2  12800  bj-uniex2  12806  bj-d0clsepcl  12815