Theorem rexbii 3247

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	anbi2i 624	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ 𝜓))
3	2	rexbii2 3245	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   ↔ wb 208   ∈ wcel 2110  ∃wrex 3139

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-rex 3144

This theorem is referenced by:  2rexbii  3248  2ex2rexrot  3250  rexcom4a  3251  r19.29rOLD  3256  r19.29imd  3257  rexnal2  3258  ralnex3OLD  3263  r19.41vv  3349  r19.42v  3350  r19.43  3351  rexcom  3355  rexcom13  3360  rexrot4  3362  3reeanv  3369  2ralor  3370  cbvrex2vw  3463  cbvrex2v  3466  rexcom4b  3525  rexcom4OLD  3527  ceqsrex2v  3651  clel5  3657  reu7  3723  2reu5a  3735  0el  4320  n0snor2el  4758  uni0b  4857  iuncom  4919  iuncom4  4920  iuniin  4924  dfiunv2  4953  iunab  4968  iunn0  4982  iunin2  4986  iundif2  4989  iunun  5008  iunxiun  5012  iunpwss  5022  axrep6  5190  inuni  5239  reusv2lem5  5295  iunopab  5439  dffr2  5515  frc  5516  frminex  5530  dfepfr  5535  epfrc  5536  xpiundi  5617  xpiundir  5618  reliin  5685  iunxpf  5714  cnvuni  5752  dmiun  5777  dmopab2rex  5781  elres  5886  elidinxp  5906  dfima3  5927  dffr3  5957  rniun  6001  xpdifid  6020  dminxp  6032  imaco  6099  coiun  6104  dffr4  6159  tz6.26  6174  sucel  6259  isarep1  6437  rexrn  6848  ralrn  6849  elrnrexdmb  6851  fnasrn  6902  rexima  6993  ralima  6994  abrexco  6997  imaiun  6998  fliftcnv  7058  rexrnmpo  7284  iunpw  7487  abrexex2g  7659  el2xptp  7729  rdglem1  8045  tz7.49  8075  oarec  8182  omeu  8205  qsid  8357  eroveu  8386  ixp0  8489  fimax2g  8758  marypha2lem2  8894  dfsup2  8902  infcllem  8945  dfoi  8969  wemapsolem  9008  zfregcl  9052  zfreg  9053  zfregfr  9062  oemapso  9139  zfregs2  9169  infenaleph  9511  isinfcard  9512  kmlem7  9576  kmlem13  9582  fin23lem26  9741  dffin1-5  9804  fin12  9829  numth  9888  ac6n  9901  zorn2lem7  9918  zorng  9920  brdom7disj  9947  brdom6disj  9948  uniwun  10156  axgroth5  10240  axgroth4  10248  grothprim  10250  npomex  10412  genpass  10425  elreal  10547  dfinfre  11616  infrenegsup  11618  uzwo  12305  ublbneg  12327  xrinfmss2  12698  4fvwrd4  13021  fsuppmapnn0fiubex  13354  fsuppmapnn0ub  13357  mptnn0fsuppr  13361  hashge2el2dif  13832  dfrtrclrec2  14410  rexanuz  14699  rexfiuz  14701  clim0  14857  cbvsum  15046  incexc2  15187  cbvprod  15263  fprodle  15344  iprodmul  15351  divalglem10  15747  divalgb  15749  ncoprmlnprm  16062  pythagtriplem2  16148  pythagtriplem19  16164  pythagtrip  16165  pceu  16177  prmreclem6  16251  4sqlem12  16286  cshwshashlem1  16423  cshwshash  16432  imasaddfnlem  16795  isdrs2  17543  smndex1mgm  18066  smndex1n0mnd  18071  pmtrprfvalrn  18610  pgpfac1lem5  19195  dvdsrval  19389  opprunit  19405  lsmspsn  19850  lsmelval2  19851  islpidl  20013  mat1dimelbas  21074  mat1dimbas  21075  mdetunilem8  21222  pmatcollpw2lem  21379  tgval2  21558  ntreq0  21679  isclo2  21690  neiptopnei  21734  ist0-3  21947  tgcmp  22003  cmpfi  22010  is1stc2  22044  unisngl  22129  xkobval  22188  txtube  22242  txcmplem1  22243  xkococnlem  22261  eltsms  22735  metrest  23128  iscau3  23875  bcth  23926  pmltpc  24045  itg2i1fseq  24350  itg2cn  24358  plyun0  24781  aaliou3lem9  24933  1cubr  25414  dchrvmasumlema  26070  selbergsb  26145  ostth  26209  istrkg2ld  26240  tglowdim1i  26281  legtrid  26371  midex  26517  ishpg  26539  brbtwn2  26685  colinearalg  26690  ax5seg  26718  axpasch  26721  axlowdimlem6  26727  axeuclidlem  26742  axeuclid  26743  elntg2  26765  umgr2edg1  26987  umgr2edgneu  26990  nbgrsym  27139  isuvtx  27171  usgr2pth0  27540  wlkiswwlksupgr2  27649  clwwlknun  27885  4cycl2vnunb  28063  fusgreg2wsp  28109  lpni  28251  nmobndseqi  28550  hhcmpl  28971  shne0i  29219  nmcopexi  29798  nmcfnexi  29822  cdj3lem3b  30211  rexcom4f  30228  reuxfrdf  30249  iunin1f  30303  ofpreima  30404  fpwrelmapffslem  30462  tosglblem  30651  xrnarchi  30808  lsmsnorb  30940  ordtconnlem1  31162  lmdvg  31191  esumfsup  31324  reprsuc  31881  reprdifc  31893  bnj168  31995  bnj1185  32060  bnj1542  32124  bnj865  32190  bnj916  32200  bnj983  32218  bnj1176  32272  bnj1189  32276  bnj1296  32288  bnj1398  32301  bnj1450  32317  bnj1463  32322  loop1cycl  32379  cvmliftlem15  32540  cvmlift2lem12  32556  satfvsuclem2  32602  satfvsucsuc  32607  satfdm  32611  satf0  32614  dmopab3rexdif  32647  dffr5  32984  imaindm  33017  dfon2lem9  33031  frpomin2  33074  soseq  33091  frrlem9  33126  noseponlem  33166  nosepon  33167  nolt02o  33194  brbigcup  33354  elfuns  33371  brimage  33382  brimg  33393  dfrecs2  33406  imagesset  33409  brub  33410  brsegle  33564  filnetlem4  33724  bj-rexcom4bv  34193  bj-rexcom4b  34194  bj-elsngl  34275  bj-rest10  34373  bj-restreg  34384  bj-mpomptALT  34405  nlpineqsn  34683  fvineqsneq  34687  iundif1  34860  matunitlindflem1  34882  poimirlem1  34887  poimirlem30  34916  poimirlem32  34918  poimir  34919  ismblfin  34927  volsupnfl  34931  itg2addnclem3  34939  fdc  35014  isfldidl  35340  eldmqsres2  35538  n0elqs  35577  rnxrncnvepres  35642  rnxrnidres  35643  dfcoels  35669  br1cossinres  35681  br1cossinidres  35683  br1cossincnvepres  35684  br1cossxrnidres  35685  br1cossxrncnvepres  35686  br1cossxrncnvssrres  35742  eldmqs1cossres  35887  prtlem10  35995  prter2  36011  islshpat  36147  lshpsmreu  36239  2dim  36600  islpln5  36665  lplnexatN  36693  islvol5  36709  dalem18  36811  dalem20  36823  lhpexle2  37140  lhpexle3  37142  lhpex2leN  37143  4atex2  37207  4atex2-0bOLDN  37209  cdlemftr3  37695  cdlemg17pq  37802  cdlemg19  37814  cdlemg21  37816  cdlemg33d  37839  dva1dim  38115  dih1dimatlem  38459  dihglb2  38472  dvh2dim  38575  mapdrvallem2  38775  mapdpglem3  38805  hdmapglem7a  39057  iunsn  39111  dffltz  39264  elrfirn  39285  isnacs2  39296  isnacs3  39300  sbc2rex  39377  4rexfrabdioph  39388  eldioph4b  39401  fphpd  39406  fiphp3d  39409  rencldnfilem  39410  rmxdioph  39606  expdiophlem1  39611  islnm2  39671  elimaint  39986  cnviun  39988  imaiun1  39989  coiun1  39990  elintima  39991  briunov2  40020  clsk3nimkb  40383  expandrexn  40620  prmunb2  40636  zfregs2VD  41168  evth2f  41265  evthf  41277  ndisj2  41306  fnlimabslt  41952  climbddf  41960  limsupub  41977  limsuppnflem  41983  limsupubuz  41986  limsupre2lem  41997  limsupreuz  42010  limsupvaluz2  42011  cnrefiisplem  42102  cnrefiisp  42103  stoweidlem28  42306  fourierdlem63  42447  fourierdlem65  42449  fourierdlem89  42473  fourierdlem90  42474  fourierdlem91  42475  fourierdlem100  42484  sge0pnfmpt  42720  ovn0  42841  smfaddlem1  43032  smflimlem4  43043  2rexsb  43292  2rexrsb  43293  cbvrex2  43295  2reu8i  43305  copisnmnd  44069  pgrpgt2nabl  44407  islindeps  44501  lindslinindsimp1  44505  lindslinindsimp2  44511  islindeps2  44531  islininds2  44532  isldepslvec2  44533  ldepslinc  44557