Theorem rexbii 3240

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

Syntax hints:   ↔ wb 197   ∈ wcel 2157  ∃wrex 3108

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

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-rex 3113

This theorem is referenced by:  2rexbii  3241  rexnal2  3242  ralnex3  3245  r19.29r  3272  r19.29imd  3273  r19.41vv  3290  r19.42v  3291  r19.43  3292  rexcom13  3300  rexrot4  3302  3reeanv  3307  2ralor  3308  cbvrex2v  3380  rexcom4  3430  rexcom4a  3431  rexcom4b  3432  ceqsrex2v  3543  reu7  3610  0el  4151  n0snor2el  4563  uni0b  4668  iuncom  4730  iuncom4  4731  iuniin  4734  dfiunv2  4759  iunab  4769  iunn0  4783  iunin2  4787  iundif2  4790  iunun  4807  iunxiun  4811  iunpwss  4821  inuni  5031  reusv2lem5  5084  reuxfrd  5103  iunopab  5220  dffr2  5289  frc  5290  frminex  5304  dfepfr  5309  epfrc  5310  xpiundi  5387  xpiundir  5388  reliin  5456  iunxpf  5486  cnvuni  5524  dmiun  5548  elres  5652  elidinxp  5674  elridOLD  5677  dfima3  5693  dffr3  5722  rniun  5768  xpdifid  5787  dminxp  5799  imaco  5868  coiun  5873  dffr4  5923  tz6.26  5938  sucel  6024  isarep1  6198  rexrn  6593  ralrn  6594  elrnrexdmb  6596  fnasrn  6644  rexima  6732  ralima  6733  abrexco  6736  imaiun  6737  fliftcnv  6795  rexrnmpt2  7016  iunpw  7218  abrexex2g  7384  abrexex2OLD  7390  el2xptp  7453  rdglem1  7757  tz7.49  7786  oarec  7889  omeu  7912  qsid  8058  eroveu  8088  ixp0  8188  fimax2g  8455  marypha2lem2  8591  dfsup2  8599  infcllem  8642  dfoi  8665  wemapsolem  8704  zfregcl  8748  zfreg  8749  zfregfr  8758  oemapso  8836  zfregs2  8866  infenaleph  9207  isinfcard  9208  kmlem7  9273  kmlem13  9279  fin23lem26  9442  dffin1-5  9505  fin12  9530  numth  9589  ac6n  9602  zorn2lem7  9619  zorng  9621  brdom7disj  9648  brdom6disj  9649  uniwun  9857  axgroth5  9941  axgroth4  9949  grothprim  9951  npomex  10113  genpass  10126  elreal  10247  dfinfre  11299  infrenegsup  11301  uzwo  11990  ublbneg  12012  xrinfmss2  12379  4fvwrd4  12703  fsuppmapnn0fiubex  13035  fsuppmapnn0ub  13038  mptnn0fsuppr  13042  hashge2el2dif  13499  wrdlen1  13575  dfrtrclrec2  14040  rexanuz  14328  rexfiuz  14330  clim0  14480  cbvsum  14668  incexc2  14812  cbvprod  14886  fprodle  14967  iprodmul  14974  divalglem10  15365  divalgb  15367  ncoprmlnprm  15673  phisum  15732  pythagtriplem2  15759  pythagtriplem19  15775  pythagtrip  15776  pceu  15788  prmreclem6  15862  4sqlem12  15897  cshwshashlem1  16034  cshwshash  16043  imasaddfnlem  16413  isdrs2  17164  symgmov1  18033  pmtrprfvalrn  18129  pgpfac1lem5  18700  dvdsrval  18867  opprunit  18883  lsmspsn  19311  lsmelval2  19312  islpidl  19475  mat1dimelbas  20509  mat1dimbas  20510  mdetunilem8  20657  pmatcollpw2lem  20816  tgval2  20995  ntreq0  21116  isclo2  21127  neiptopnei  21171  ist0-3  21384  tgcmp  21439  cmpfi  21446  is1stc2  21480  unisngl  21565  xkobval  21624  txtube  21678  txcmplem1  21679  xkococnlem  21697  eltsms  22170  metrest  22563  iscau3  23310  bcth  23360  pmltpc  23454  itg2i1fseq  23759  itg2cn  23767  plyun0  24190  aaliou3lem9  24342  1cubr  24806  dchrvmasumlema  25426  selbergsb  25501  ostth  25565  istrkg2ld  25596  tglowdim1i  25633  tgdim01  25639  legtrid  25723  midex  25866  ishpg  25888  brbtwn2  26022  colinearalg  26027  ax5seg  26055  axpasch  26058  axlowdimlem6  26064  axeuclidlem  26079  axeuclid  26080  umgr2edg1  26341  umgr2edgneu  26344  nbgrsym  26502  nbgrsymOLD  26503  isuvtx  26538  isuvtxaOLD  26539  usgr2pth0  26912  wlkiswwlksupgr2  27027  clwwlknun  27304  clwwlknunOLD  27309  4cycl2vnunb  27488  fusgreg2wsp  27534  lpni  27686  nmobndseqi  27985  hhcmpl  28408  shne0i  28658  nmcopexi  29237  nmcfnexi  29261  cdj3lem3b  29650  rexcom4f  29668  iunin1f  29722  ofpreima  29815  fpwrelmapffslem  29857  tosglblem  30017  xrnarchi  30086  ordtconnlem1  30318  lmdvg  30347  esumfsup  30480  reprsuc  31041  reprdifc  31053  bnj168  31144  bnj1185  31209  bnj1542  31272  bnj865  31338  bnj916  31348  bnj983  31366  bnj1176  31418  bnj1189  31422  bnj1296  31434  bnj1398  31447  bnj1450  31463  bnj1463  31468  cvmliftlem15  31625  cvmlift2lem12  31641  dffr5  31987  imaindm  32024  dfon2lem9  32038  frpomin2  32082  soseq  32097  noseponlem  32160  nosepon  32161  nolt02o  32188  brbigcup  32348  elfuns  32365  brimage  32376  brimg  32387  dfrecs2  32400  imagesset  32403  brub  32404  brsegle  32558  gtinfOLD  32657  filnetlem4  32719  bj-rexcom4a  33197  bj-rexcom4bv  33198  bj-rexcom4b  33199  bj-elsngl  33285  bj-rest10  33371  bj-restreg  33382  bj-mpt2mptALT  33402  iundif1  33715  matunitlindflem1  33737  poimirlem1  33742  poimirlem30  33771  poimirlem32  33773  poimir  33774  ismblfin  33782  volsupnfl  33786  itg2addnclem3  33794  fdc  33871  isfldidl  34197  eldmqsres2  34388  n0elqs  34432  rnxrncnvepres  34490  rnxrnidres  34491  dfcoels  34517  br1cossinres  34529  br1cossinidres  34531  br1cossincnvepres  34532  br1cossxrnidres  34533  br1cossxrncnvepres  34534  br1cossxrncnvssrres  34590  prtlem10  34663  prter2  34679  islshpat  34816  lshpsmreu  34908  2dim  35269  islpln5  35334  lplnexatN  35362  islvol5  35378  dalem18  35480  dalem20  35492  lhpexle2  35809  lhpexle3  35811  lhpex2leN  35812  4atex2  35876  4atex2-0bOLDN  35878  cdlemftr3  36364  cdlemg17pq  36471  cdlemg19  36483  cdlemg21  36485  cdlemg33d  36508  dva1dim  36784  dih1dimatlem  37128  dihglb2  37141  dvh2dim  37244  mapdrvallem2  37444  mapdpglem3  37474  hdmapglem7a  37726  elrfirn  37778  isnacs2  37789  isnacs3  37793  sbc2rex  37871  4rexfrabdioph  37882  eldioph4b  37895  fphpd  37900  fiphp3d  37903  rencldnfilem  37904  rmxdioph  38102  expdiophlem1  38107  islnm2  38167  elimaint  38458  cnviun  38460  imaiun1  38461  coiun1  38462  elintima  38463  briunov2  38492  clsk3nimkb  38856  prmunb2  39028  zfregs2VD  39588  evth2f  39686  evthf  39698  ndisj2  39729  fnlimabslt  40409  climbddf  40417  limsupub  40434  limsuppnflem  40440  limsupubuz  40443  limsupre2lem  40454  limsupreuz  40467  limsupvaluz2  40468  cnrefiisplem  40553  cnrefiisp  40554  stoweidlem28  40742  fourierdlem63  40883  fourierdlem65  40885  fourierdlem89  40909  fourierdlem90  40910  fourierdlem91  40911  fourierdlem100  40920  sge0pnfmpt  41159  ovn0  41280  smfaddlem1  41471  smflimlem4  41482  2rexsb  41701  2rexrsb  41702  cbvrex2  41704  2reu5a  41707  copisnmnd  42395  pgrpgt2nabl  42733  islindeps  42828  lindslinindsimp1  42832  lindslinindsimp2  42838  islindeps2  42858  islininds2  42859  isldepslvec2  42860  ldepslinc  42884