Theorem rexbii 3113

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 3111	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2147  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3091

This theorem is used by:  r19.29imd  3131  r19.43  3134  3r19.43  3135  2rexbii  3142  rexnal2  3148  r19.42v  3198  r19.41vv  3236  3reeanv  3239  cbvrex2vw  3249  rexcom4a  3296  rexcom13  3299  rexrot4  3300  2ex2rexrot  3301  cbvrex2v  3358  rexcom4b  3485  ceqsrex2v  3615  clel5  3622  reu7  3693  2reu5a  3705  0el  4314  n0snor2el  4791  uni0b  4897  iuncom  4962  iuncom4  4963  iuniin  4967  dfiunv2  4995  iunab  5013  iunid  5022  iunsn  5027  iunn0  5028  iunin2  5032  iundif2  5035  iunun  5056  iunxiun  5060  iunpwss  5070  inuni  5316  reusv2lem5  5369  iunopab  5539  dffr2  5617  dffr2ALT  5618  frc  5619  frminex  5635  dfepfr  5640  epfrc  5641  xpiundi  5727  xpiundir  5728  reliin  5801  el2xptp  5827  iunxpf  5833  cnvuni  5876  dmiun  5903  dmopab2rex  5907  elres  6022  elidinxp  6049  dfima3  6072  dffr3  6110  rniun  6152  xpdifid  6172  xpdifcnvepel  6173  dminxp  6185  imaco  6266  coiun  6272  imaindm  6323  dffr4  6344  frpomin2  6365  sucel  6460  isarep1  6653  rexrn  7114  ralrn  7115  elrnrexdmb  7117  fnasrn  7175  ralima  7269  abrexco  7274  imaiun  7275  fliftcnv  7345  rexrnmpo  7587  imaeqexov  7686  mpt3mpt  7712  iunpw  7812  abrexex2g  8003  reldm  8082  poxp2  8190  poxp3  8197  soseq  8206  frrlem9  8343  rdglem1  8454  tz7.49  8486  oarec  8601  omeu  8624  qsid  8833  eroveu  8864  ixp0  8990  fimax2g  9308  marypha2lem2  9458  dfsup2  9466  infcllem  9510  dfoi  9535  wemapsolem  9574  zfregcl  9618  zfregclOLD  9619  zfreg  9620  zfregfr  9635  oemapso  9713  brttrcl2  9745  ttrclresv  9748  zfregs2  9764  infenaleph  10200  isinfcard  10201  kmlem7  10265  kmlem13  10271  fin23lem26  10433  dffin1-5  10496  fin12  10521  numth  10580  ac6n  10593  zorn2lem7  10610  zorng  10612  brdom7disj  10640  brdom6disj  10641  uniwun  10855  axgroth5  10939  axgroth4  10947  grothprim  10949  npomex  11111  genpass  11124  elreal  11246  dfinfre  12328  infrenegsup  12330  uzwo  13068  ublbneg  13090  xrinfmss2  13471  4fvwrd4  13812  fsuppmapnn0fiubex  14165  fsuppmapnn0ub  14168  mptnn0fsuppr  14172  hashge2el2dif  14655  cshwsexa  15006  dfrtrclrec2  15243  rexanuz  15545  rexfiuz  15547  clim0  15705  cbvsum  15894  cbvsumv  15895  incexc2  16039  cbvprod  16114  cbvprodv  16115  prodeq1i  16117  fprodle  16195  iprodmul  16202  divalglem10  16604  divalgb  16606  ncoprmlnprm  16936  pythagtriplem2  17027  pythagtriplem19  17043  pythagtrip  17044  pceu  17056  prmreclem6  17131  4sqlem12  17166  cshwshashlem1  17305  cshwshash  17314  imasaddfnlem  17732  isdrs2  18512  chnfi  18840  smndex1mgm  19138  smndex1n0mnd  19143  pmtrprfvalrn  19735  pgpfac1lem5  20328  dvdsrval  20624  opprunit  20640  isdrng4  21025  isdrng3lem1  21038  lsmspsn  21392  lsmelval2  21393  islpidl  21682  pzriprnglem3  21822  pzriprnglem10  21829  mat1dimelbas  22819  mat1dimbas  22820  mdetunilem8  22967  matunitlindflem1  23027  pmatcollpw2lem  23128  tgval2  23307  ntreq0  23428  isclo2  23439  neiptopnei  23483  ist0-3  23696  tgcmp  23752  cmpfi  23759  is1stc2  23793  unisngl  23879  xkobval  23938  txtube  23992  txcmplem1  23993  xkococnlem  24011  eltsms  24485  metrest  24876  iscau3  25632  bcth  25683  pmltpc  25804  itg2i1fseq  26109  itg2cn  26117  plyun0  26548  plyconz  26664  aaliou3lem9  26710  1cubr  27203  dchrvmasumlema  27860  selbergsb  27935  ostth  27999  noseponlem  28054  nosepon  28055  nolt02o  28085  noinfbnd1lem1  28113  noinfbnd1lem4  28116  cuteq1  28236  elold  28278  made0  28282  lrrecfr  28362  leadds1  28408  addsuniflem  28420  addsasslem1  28422  addsasslem2  28423  mulsrid  28532  mulsuniflem  28568  addsdilem1  28570  addsdilem2  28571  mulsasslem1  28582  mulsasslem2  28583  z12sge0  28902  elreno2  28914  renegscl  28917  istrkg2ld  28955  tglowdim1i  28997  legtrid  29087  midex  29246  ishpg  29270  brbtwn2  29516  colinearalg  29521  ax5seg  29549  axpasch  29552  axlowdimlem6  29558  axeuclidlem  29573  axeuclid  29574  elntg2  29596  umgr2edg1  29825  umgr2edgneu  29828  nbgrsym  29977  isuvtx  30009  usgr2pth0  30384  wlkiswwlksupgr2  30499  clwwlknun  30736  loop1cycl  30777  4cycl2vnunb  30924  fusgreg2wsp  30970  lpni  31115  nmobndseqi  31414  hhcmpl  31835  shne0i  32083  nmcopexi  32662  nmcfnexi  32686  cdj3lem3b  33075  rexcom4f  33140  reuxfrdf  33162  iunin1f  33227  ofpreima  33334  intimafv  33378  fpwrelmapffslem  33397  tosglblem  33608  xrnarchi  33821  isunit2  33876  dvdsrspss  34026  lsmsnorb  34030  lsmsnorb2  34031  1arithufdlem4  34163  constrconj  34460  ordtconnlem1  34639  lmdvg  34668  esumfsup  34785  reprsuc  35327  reprdifc  35339  bnj168  35444  bnj1185  35506  bnj1542  35570  bnj865  35636  bnj916  35646  bnj983  35664  bnj1176  35718  bnj1189  35722  bnj1296  35734  bnj1398  35747  bnj1450  35763  bnj1463  35768  nummin  35819  fineqvnttrclse  35905  axregszf  35910  onvf1odlem1  36044  cvmliftlem15  36243  cvmlift2lem12  36259  satfvsuclem2  36305  satfvsucsuc  36310  satfdm  36314  satf0  36317  dmopab3rexdif  36350  rexxfr3dALT  36584  dffr5  36710  dfon2lem9  36744  brbigcup  36851  elfuns  36868  brimage  36879  brimg  36890  dfrecs2  36905  imagesset  36908  brub  36909  dffr7  36911  brsegle  37064  sumeq2si  37182  prodeq2si  37184  cbvprodvw2  37227  filnetlem4  37360  bj-rexcom4bv  37985  bj-rexcom4b  37986  bj-elsngl  38072  bj-elinxp  38151  bj-elres  38153  bj-axseprep  38194  bj-rest10  38213  bj-restreg  38224  bj-mpomptALT  38245  nlpineqsn  38536  fvineqsneq  38540  iundif1  38727  poimirlem1  38744  poimirlem30  38773  poimirlem32  38775  poimir  38776  ismblfin  38784  volsupnfl  38788  itg2addnclem3  38796  dfproplem  38846  fdc  38882  isfldidl  39205  eldmqsres2  39429  n0elqs  39467  rnxrncnvepres  39558  rnxrnidres  39559  dfcoels  39655  br1cossinres  39672  br1cossinidres  39674  br1cossincnvepres  39675  br1cossxrnidres  39676  br1cossxrncnvepres  39677  br1cossxrncnvssrres  39723  eldmqs1cossres  39879  disjdmqscossss  40041  prtlem10  40125  prter2  40141  islshpat  40277  lshpsmreu  40369  2dim  40730  islpln5  40795  lplnexatN  40823  islvol5  40839  dalem18  40941  dalem20  40953  lhpexle2  41270  lhpexle3  41272  lhpex2leN  41273  4atex2  41337  4atex2-0bOLDN  41339  cdlemftr3  41825  cdlemg17pq  41932  cdlemg19  41944  cdlemg21  41946  cdlemg33d  41969  dva1dim  42245  dih1dimatlem  42589  dihglb2  42602  dvh2dim  42705  mapdrvallem2  42905  mapdpglem3  42935  hdmapglem7a  43187  hashnexinjle  43382  aks6d1c5  43392  supinf  43497  fimgmcyclem  43801  dffltz  43874  elrfirn  43910  isnacs2  43921  isnacs3  43925  sbc2rex  44000  4rexfrabdioph  44009  eldioph4b  44022  fphpd  44027  fiphp3d  44030  rencldnfilem  44031  rmxdioph  44227  expdiophlem1  44232  islnm2  44284  onmaxnelsup  44428  onsupnmax  44433  onsupuni  44434  onsupmaxb  44444  tfsconcatlem  44541  tfsconcatrn  44547  oadif1lem  44584  oadif1  44585  elimaint  44852  cnviun  44853  imaiun1  44854  coiun1  44855  elintima  44856  briunov2  44885  clsk3nimkb  45243  expandrexn  45478  prmunb2  45498  zfregs2VD  46025  n0abso  46172  sswfaxreg  46183  evth2f  46248  evthf  46260  ndisj2  46284  rexanuz2nf  46717  fnlimabslt  46904  climbddf  46912  limsupub  46929  limsuppnflem  46935  limsupubuz  46938  limsupre2lem  46949  limsupreuz  46962  limsupvaluz2  46963  cnrefiisplem  47054  cnrefiisp  47055  stoweidlem28  47253  fourierdlem63  47394  fourierdlem65  47396  fourierdlem89  47420  fourierdlem90  47421  fourierdlem91  47422  fourierdlem100  47431  sge0pnfmpt  47670  ovn0  47791  smfaddlem1  47988  smflimlem4  47999  fsetsniunop  48334  2rexsb  48387  2rexrsb  48388  cbvrex2  48390  2reu8i  48399  clnbgrsym  49151  isubgr3stgrlem6  49284  copisnmnd  49481  pgrpgt2nabl  49693  islindeps  49780  lindslinindsimp1  49784  lindslinindsimp2  49790  islindeps2  49810  islininds2  49811  isldepslvec2  49812  ldepslinc  49836  sepnsepolem1  50251  ralsbii  51209