Theorem rexbidva 3177

Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 9-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 6-Dec-2019.) (Proof shortened by Wolf Lammen, 10-Dec-2019.)

Hypothesis

Ref	Expression
ralbidva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rexbidva	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rexbidva

Step	Hyp	Ref	Expression
1		ralbidva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
2	1	pm5.32da 580	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
3	2	rexbidv2 3175	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   ∈ wcel 2107  ∃wrex 3071

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  rexbidv  3179  2rexbiia  3216  2rexbidva  3218  rexeqbidva  3329  frinxp  5759  onfr  6404  dfimafn  6955  funimass4  6957  fliftel  7306  fliftf  7312  isomin  7334  f1oiso  7348  releldm2  8029  oaass  8561  eldifsucnn  8663  cofonr  8673  naddunif  8692  qsinxp  8787  qliftel  8794  fimaxg  9290  ordunifi  9293  supisolem  9468  fiming  9493  wemapwe  9692  ttrcltr  9711  ttrclse  9722  frmin  9744  cflim2  10258  cfsmolem  10265  alephsing  10271  brdom7disj  10526  brdom6disj  10527  alephreg  10577  nqereu  10924  1idpr  11024  map2psrpr  11105  axsup  11289  rereccl  11932  sup3  12171  infm3  12173  supadd  12182  creur  12206  creui  12207  nndiv  12258  nnrecl  12470  rpnnen1lem2  12961  rpnnen1lem1  12962  rpnnen1lem3  12963  rpnnen1lem5  12965  supxrbnd1  13300  supxrbnd2  13301  supxrbnd  13307  rabssnn0fi  13951  mptnn0fsupp  13962  expnlbnd  14196  wrdl3s3  14913  limsuplt  15423  clim2  15448  clim2c  15449  clim0c  15451  ello12  15460  elo12  15471  rlimresb  15509  climabs0  15529  sumeq2ii  15639  mertens  15832  prodeq2ii  15857  zprod  15881  nndivides  16207  alzdvds  16263  oddm1even  16286  oddnn02np1  16291  oddge22np1  16292  evennn02n  16293  evennn2n  16294  divalglem4  16339  divalgb  16347  modremain  16351  modprmn0modprm0  16740  vdwlem6  16919  vdwlem11  16924  vdw  16927  ramval  16941  imasleval  17487  dfiso3  17720  fullestrcsetc  18103  fullsetcestrc  18118  isipodrs  18490  ipodrsfi  18492  gsumpropd2lem  18598  mndpropd  18650  grppropd  18837  qus0subgbas  19075  conjnmzb  19127  symgextfo  19290  symgfixfo  19307  sylow1lem2  19467  sylow3lem1  19495  sylow3lem3  19497  lsmelvalm  19519  lsmass  19537  iscyg3  19754  ghmcyg  19764  cycsubgcyg  19769  pgpfac1lem2  19945  pgpfac1lem4  19948  ablfac2  19959  dvdsr02  20186  crngunit  20192  dvdsrpropd  20230  lpigen  20894  znunit  21119  elfilspd  21358  scmatmats  22013  symgmatr01  22156  isclo  22591  iscnp3  22748  lmbrf  22764  cncnp  22784  lmss  22802  isnrm2  22862  cmpfi  22912  1stcfb  22949  1stccnp  22966  ptrescn  23143  txkgen  23156  xkoinjcn  23191  trfil3  23392  fmid  23464  lmflf  23509  txflf  23510  ptcmplem3  23558  tsmsf1o  23649  ucnprima  23787  metrest  24033  metcnp  24050  metcnp2  24051  txmetcnp  24056  metuel2  24074  metustbl  24075  psmetutop  24076  metucn  24080  evth2  24476  lmmbrf  24779  iscfil2  24783  fmcfil  24789  iscau2  24794  iscau4  24796  iscauf  24797  caucfil  24800  iscmet3lem3  24807  cfilresi  24812  causs  24815  lmclim  24820  ivth2  24972  ovolfioo  24984  ovolficc  24985  ovolshftlem1  25026  ovolscalem1  25030  volsup2  25122  ismbf3d  25171  mbfaddlem  25177  mbfsup  25181  mbfinf  25182  itg2seq  25260  itg2gt0  25278  ellimc2  25394  ellimc3  25396  rolle  25507  cmvth  25508  mvth  25509  dvlip  25510  dvivth  25527  lhop1lem  25530  deg1ldg  25610  ulm2  25897  ulmdvlem3  25914  dcubic  26351  mcubic  26352  cubic2  26353  rlimcnp  26470  ftalem3  26579  isppw2  26619  lgsquadlem2  26884  2lgslem1a  26894  dchrmusumlema  26996  dchrisum0lema  27017  cofcutr  27411  lrrecfr  27427  addsrid  27448  addscom  27450  addsuniflem  27484  addsass  27488  negsunif  27529  mulsrid  27569  mulsasslem3  27620  tglowdim2l  27901  mirreu3  27905  oppcom  27995  iscgra1  28061  axsegcon  28185  axpasch  28199  axcontlem7  28228  usgr2pth0  29022  usgr2wspthon  29219  elwwlks2  29220  elwspths2spth  29221  rusgrnumwwlks  29228  clwwlkfo  29303  eclclwwlkn1  29328  eucrctshift  29496  fusgreg2wsp  29589  nmobndi  30028  nmounbi  30029  nmoo0  30044  h2hcau  30232  h2hlm  30233  shsel3  30568  pjhtheu2  30669  chscllem2  30891  adjbdln  31336  branmfn  31358  pjimai  31429  chrelati  31617  cdj3lem3  31691  cdj3lem3b  31693  dfimafnf  31860  ofpreima  31890  isarchi2  32331  submarchi  32332  archirng  32334  archiabl  32344  isarchiofld  32435  ellspds  32481  lsmssass  32512  grplsm0l  32513  fedgmullem2  32715  elirng  32750  zarcls  32854  ordtconnlem1  32904  lmdvg  32933  esumfsup  33068  dya2icoseg2  33277  eulerpartlemgh  33377  ballotlemodife  33496  ballotlemsima  33514  nummin  34094  erdszelem10  34191  iscvm  34250  wsuclem  34797  seglelin  35088  outsideofeu  35103  gg-cmvth  35181  opnrebl  35205  opnrebl2  35206  filnetlem4  35266  bj-finsumval0  36166  phpreu  36472  ptrest  36487  poimirlem3  36491  poimirlem4  36492  poimirlem17  36505  poimirlem26  36514  poimirlem27  36515  broucube  36522  mblfinlem1  36525  lmclim2  36626  caures  36628  isbnd3b  36653  heiborlem7  36685  heiborlem10  36688  rrncmslem  36700  isdrngo2  36826  erimeq2  37548  prter3  37752  islshpsm  37850  lsatfixedN  37879  lrelat  37884  eqlkr2  37970  lshpkrlem1  37980  lfl1dim  37991  eqlkr4  38035  ishlat3N  38224  hlsupr2  38258  hlrelat5N  38272  hlrelat  38273  cvrval5  38286  cvrat42  38315  athgt  38327  3dim0  38328  islln3  38381  llnexatN  38392  islpln3  38404  islvol3  38447  islvol5  38450  isline4N  38648  polval2N  38777  4atex3  38952  cdleme0ex2N  39095  cdlemefrs29cpre1  39269  cdlemb3  39477  cdlemg33c  39579  cdlemg33e  39581  dia1dim2  39933  cdlemm10N  39989  dib1dim2  40039  diclspsn  40065  dih1dimatlem  40200  dihatexv2  40210  djhcvat42  40286  dihjat1lem  40299  dvh4dimat  40309  dvh2dimatN  40311  lcfrlem9  40421  mapdval4N  40503  mapdcv  40531  infdesc  41385  elrfirn  41433  elrfirn2  41434  mrefg3  41446  diophin  41510  diophun  41511  diophren  41551  rmxycomplete  41656  wepwsolem  41784  fnwe2lem2  41793  islssfg  41812  unielss  41967  onmaxnelsup  41972  onsupnmax  41977  onsupeqnmax  41996  tfsconcat0i  42095  ntrneineine0lem  42834  ntrneineine1lem  42835  ntrneiel2  42837  extoimad  42916  grumnudlem  43044  supsubc  44063  infxrbnd2  44079  supminfxr  44174  evthiccabs  44209  elicores  44246  clim2f  44352  clim2cf  44366  clim0cf  44370  clim2f2  44386  limsupub  44420  limsupmnflem  44436  limsupre2lem  44440  limsuplt2  44469  liminfreuzlem  44518  liminfltlem  44520  liminflimsupclim  44523  xlimmnfmpt  44559  xlimpnfmpt  44560  fourierdlem73  44895  fourierdlem83  44905  meaiuninc3v  45200  ovolval2  45360  cfsetsnfsetfo  45770  dfaimafn  45873  iccelpart  46101  sprsymrelf  46163  sprsymrelfo  46165  fmtnoprmfac1  46233  fmtnoprmfac2  46235  fmtnofac2lem  46236  dfeven2  46317  dfodd3  46318  isomuspgrlem2d  46499  uspgrsprfo  46526  rngqiprngimfo  46786  pzriprnglem10  46814  elbigo2  47238  rrxlinesc  47421  rrxlinec  47422  rrx2line  47426  rrx2vlinest  47427  itsclquadeu  47463