Theorem rexbii 3182

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

Step	Hyp	Ref	Expression
1		rexbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))
3	2	rexbiia 3181	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   ↔ wb 205   ∈ wcel 2107  ∃wrex 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-rex 3071

This theorem is referenced by:  2rexbii  3183  r19.29imd  3187  rexnal2  3188  2ex2rexrot  3236  rexcom4a  3237  r19.41vv  3279  r19.42v  3280  r19.43  3281  rexcomOLD  3286  rexcom13  3288  rexrot4  3290  3reeanv  3296  2ralorOLD  3298  cbvrex2vw  3398  cbvrex2v  3401  rexcom4b  3462  ceqsrex2v  3588  clel5  3597  reu7  3668  2reu5a  3680  0el  4295  n0snor2el  4765  uni0b  4868  iuncom  4932  iuncom4  4933  iuniin  4937  dfiunv2  4966  iunab  4982  iunsn  4996  iunn0  4997  iunin2  5001  iundif2  5004  iunun  5023  iunxiun  5027  iunpwss  5037  axrep6  5217  inuni  5268  reusv2lem5  5326  iunopab  5473  iunopabOLD  5474  dffr2  5554  dffr2ALT  5555  frc  5556  frminex  5570  dfepfr  5575  epfrc  5576  xpiundi  5658  xpiundir  5659  reliin  5729  iunxpf  5760  cnvuni  5798  dmiun  5825  dmopab2rex  5829  elres  5933  elidinxp  5954  dfima3  5975  dffr3  6010  rniun  6056  xpdifid  6076  dminxp  6088  imaco  6159  coiun  6164  dffr4  6226  frpomin2  6248  tz6.26OLD  6255  sucel  6343  isarep1  6530  isarep1OLD  6531  rexrn  6972  ralrn  6973  elrnrexdmb  6975  fnasrn  7026  rexima  7122  ralima  7123  abrexco  7126  imaiun  7127  fliftcnv  7191  rexrnmpo  7422  iunpw  7630  abrexex2g  7816  el2xptp  7886  frrlem9  8119  rdglem1  8255  tz7.49  8285  oarec  8402  omeu  8425  qsid  8581  eroveu  8610  ixp0  8728  fimax2g  9069  marypha2lem2  9204  dfsup2  9212  infcllem  9255  dfoi  9279  wemapsolem  9318  zfregcl  9362  zfreg  9363  zfregfr  9372  oemapso  9449  brttrcl2  9481  ttrclresv  9484  zfregs2  9500  infenaleph  9856  isinfcard  9857  kmlem7  9921  kmlem13  9927  fin23lem26  10090  dffin1-5  10153  fin12  10178  numth  10237  ac6n  10250  zorn2lem7  10267  zorng  10269  brdom7disj  10296  brdom6disj  10297  uniwun  10505  axgroth5  10589  axgroth4  10597  grothprim  10599  npomex  10761  genpass  10774  elreal  10896  dfinfre  11965  infrenegsup  11967  uzwo  12660  ublbneg  12682  xrinfmss2  13054  4fvwrd4  13385  fsuppmapnn0fiubex  13721  fsuppmapnn0ub  13724  mptnn0fsuppr  13728  hashge2el2dif  14203  dfrtrclrec2  14778  rexanuz  15066  rexfiuz  15068  clim0  15224  cbvsum  15416  incexc2  15559  cbvprod  15634  fprodle  15715  iprodmul  15722  divalglem10  16120  divalgb  16122  ncoprmlnprm  16441  pythagtriplem2  16527  pythagtriplem19  16543  pythagtrip  16544  pceu  16556  prmreclem6  16631  4sqlem12  16666  cshwshashlem1  16806  cshwshash  16815  imasaddfnlem  17248  isdrs2  18033  smndex1mgm  18555  smndex1n0mnd  18560  pmtrprfvalrn  19105  pgpfac1lem5  19691  dvdsrval  19896  opprunit  19912  lsmspsn  20355  lsmelval2  20356  islpidl  20526  mat1dimelbas  21629  mat1dimbas  21630  mdetunilem8  21777  pmatcollpw2lem  21935  tgval2  22115  ntreq0  22237  isclo2  22248  neiptopnei  22292  ist0-3  22505  tgcmp  22561  cmpfi  22568  is1stc2  22602  unisngl  22687  xkobval  22746  txtube  22800  txcmplem1  22801  xkococnlem  22819  eltsms  23293  metrest  23689  iscau3  24451  bcth  24502  pmltpc  24623  itg2i1fseq  24929  itg2cn  24937  plyun0  25367  aaliou3lem9  25519  1cubr  26001  dchrvmasumlema  26657  selbergsb  26732  ostth  26796  istrkg2ld  26830  tglowdim1i  26871  legtrid  26961  midex  27107  ishpg  27129  brbtwn2  27282  colinearalg  27287  ax5seg  27315  axpasch  27318  axlowdimlem6  27324  axeuclidlem  27339  axeuclid  27340  elntg2  27362  umgr2edg1  27587  umgr2edgneu  27590  nbgrsym  27739  isuvtx  27771  usgr2pth0  28142  wlkiswwlksupgr2  28251  clwwlknun  28485  4cycl2vnunb  28663  fusgreg2wsp  28709  lpni  28851  nmobndseqi  29150  hhcmpl  29571  shne0i  29819  nmcopexi  30398  nmcfnexi  30422  cdj3lem3b  30811  rexcom4f  30828  reuxfrdf  30848  iunin1f  30906  ofpreima  31011  intimafv  31052  fpwrelmapffslem  31076  tosglblem  31261  xrnarchi  31447  lsmsnorb  31588  lsmsnorb2  31589  ordtconnlem1  31883  lmdvg  31912  esumfsup  32047  reprsuc  32604  reprdifc  32616  bnj168  32718  bnj1185  32782  bnj1542  32846  bnj865  32912  bnj916  32922  bnj983  32940  bnj1176  32994  bnj1189  32998  bnj1296  33010  bnj1398  33023  bnj1450  33039  bnj1463  33044  nummin  33072  loop1cycl  33108  cvmliftlem15  33269  cvmlift2lem12  33285  satfvsuclem2  33331  satfvsucsuc  33336  satfdm  33340  satf0  33343  dmopab3rexdif  33376  imaeqsexv  33699  dffr5  33730  imaindm  33762  dfon2lem9  33776  poxp2  33799  poxp3  33805  soseq  33812  noseponlem  33876  nosepon  33877  nolt02o  33907  noinfbnd1lem1  33935  noinfbnd1lem4  33938  elold  34062  made0  34066  lrrecfr  34109  brbigcup  34209  elfuns  34226  brimage  34237  brimg  34248  dfrecs2  34261  imagesset  34264  brub  34265  brsegle  34419  filnetlem4  34579  bj-rexcom4bv  35076  bj-rexcom4b  35077  bj-elsngl  35167  bj-rest10  35268  bj-restreg  35279  bj-mpomptALT  35299  nlpineqsn  35588  fvineqsneq  35592  iundif1  35760  matunitlindflem1  35782  poimirlem1  35787  poimirlem30  35816  poimirlem32  35818  poimir  35819  ismblfin  35827  volsupnfl  35831  itg2addnclem3  35839  fdc  35912  isfldidl  36235  eldmqsres2  36430  n0elqs  36468  rnxrncnvepres  36533  rnxrnidres  36534  dfcoels  36560  br1cossinres  36572  br1cossinidres  36574  br1cossincnvepres  36575  br1cossxrnidres  36576  br1cossxrncnvepres  36577  br1cossxrncnvssrres  36633  eldmqs1cossres  36778  prtlem10  36886  prter2  36902  islshpat  37038  lshpsmreu  37130  2dim  37491  islpln5  37556  lplnexatN  37584  islvol5  37600  dalem18  37702  dalem20  37714  lhpexle2  38031  lhpexle3  38033  lhpex2leN  38034  4atex2  38098  4atex2-0bOLDN  38100  cdlemftr3  38586  cdlemg17pq  38693  cdlemg19  38705  cdlemg21  38707  cdlemg33d  38730  dva1dim  39006  dih1dimatlem  39350  dihglb2  39363  dvh2dim  39466  mapdrvallem2  39666  mapdpglem3  39696  hdmapglem7a  39948  dffltz  40478  elrfirn  40524  isnacs2  40535  isnacs3  40539  sbc2rex  40616  4rexfrabdioph  40627  eldioph4b  40640  fphpd  40645  fiphp3d  40648  rencldnfilem  40649  rmxdioph  40845  expdiophlem1  40850  islnm2  40910  elimaint  41264  cnviun  41265  imaiun1  41266  coiun1  41267  elintima  41268  briunov2  41297  clsk3nimkb  41657  expandrexn  41916  prmunb2  41936  zfregs2VD  42468  evth2f  42565  evthf  42577  ndisj2  42606  fnlimabslt  43227  climbddf  43235  limsupub  43252  limsuppnflem  43258  limsupubuz  43261  limsupre2lem  43272  limsupreuz  43285  limsupvaluz2  43286  cnrefiisplem  43377  cnrefiisp  43378  stoweidlem28  43576  fourierdlem63  43717  fourierdlem65  43719  fourierdlem89  43743  fourierdlem90  43744  fourierdlem91  43745  fourierdlem100  43754  sge0pnfmpt  43990  ovn0  44111  smfaddlem1  44308  smflimlem4  44319  fsetsniunop  44554  2rexsb  44604  2rexrsb  44605  cbvrex2  44607  2reu8i  44616  copisnmnd  45374  pgrpgt2nabl  45713  islindeps  45805  lindslinindsimp1  45809  lindslinindsimp2  45815  islindeps2  45835  islininds2  45836  isldepslvec2  45837  ldepslinc  45861  sepnsepolem1  46226