Theorem rexbidva 3176

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 579	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
3	2	rexbidv2 3174	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∈ wcel 2106  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

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

This theorem is referenced by:  rexbidv  3178  2rexbiia  3215  2rexbidva  3217  rexeqbidva  3328  frinxp  5758  onfr  6403  dfimafn  6954  funimass4  6956  fliftel  7308  fliftf  7314  isomin  7336  f1oiso  7350  releldm2  8031  oaass  8563  eldifsucnn  8665  cofonr  8675  naddunif  8694  qsinxp  8789  qliftel  8796  fimaxg  9292  ordunifi  9295  supisolem  9470  fiming  9495  wemapwe  9694  ttrcltr  9713  ttrclse  9724  frmin  9746  cflim2  10260  cfsmolem  10267  alephsing  10273  brdom7disj  10528  brdom6disj  10529  alephreg  10579  nqereu  10926  1idpr  11026  map2psrpr  11107  axsup  11291  rereccl  11934  sup3  12173  infm3  12175  supadd  12184  creur  12208  creui  12209  nndiv  12260  nnrecl  12472  rpnnen1lem2  12963  rpnnen1lem1  12964  rpnnen1lem3  12965  rpnnen1lem5  12967  supxrbnd1  13302  supxrbnd2  13303  supxrbnd  13309  rabssnn0fi  13953  mptnn0fsupp  13964  expnlbnd  14198  wrdl3s3  14915  limsuplt  15425  clim2  15450  clim2c  15451  clim0c  15453  ello12  15462  elo12  15473  rlimresb  15511  climabs0  15531  sumeq2ii  15641  mertens  15834  prodeq2ii  15859  zprod  15883  nndivides  16209  alzdvds  16265  oddm1even  16288  oddnn02np1  16293  oddge22np1  16294  evennn02n  16295  evennn2n  16296  divalglem4  16341  divalgb  16349  modremain  16353  modprmn0modprm0  16742  vdwlem6  16921  vdwlem11  16926  vdw  16929  ramval  16943  imasleval  17489  dfiso3  17722  fullestrcsetc  18105  fullsetcestrc  18120  isipodrs  18492  ipodrsfi  18494  gsumpropd2lem  18600  mndpropd  18652  grppropd  18839  qus0subgbas  19077  conjnmzb  19129  symgextfo  19292  symgfixfo  19309  sylow1lem2  19469  sylow3lem1  19497  sylow3lem3  19499  lsmelvalm  19521  lsmass  19539  iscyg3  19756  ghmcyg  19766  cycsubgcyg  19771  pgpfac1lem2  19947  pgpfac1lem4  19950  ablfac2  19961  dvdsr02  20190  crngunit  20196  dvdsrpropd  20234  lpigen  20900  znunit  21125  elfilspd  21364  scmatmats  22020  symgmatr01  22163  isclo  22598  iscnp3  22755  lmbrf  22771  cncnp  22791  lmss  22809  isnrm2  22869  cmpfi  22919  1stcfb  22956  1stccnp  22973  ptrescn  23150  txkgen  23163  xkoinjcn  23198  trfil3  23399  fmid  23471  lmflf  23516  txflf  23517  ptcmplem3  23565  tsmsf1o  23656  ucnprima  23794  metrest  24040  metcnp  24057  metcnp2  24058  txmetcnp  24063  metuel2  24081  metustbl  24082  psmetutop  24083  metucn  24087  evth2  24483  lmmbrf  24786  iscfil2  24790  fmcfil  24796  iscau2  24801  iscau4  24803  iscauf  24804  caucfil  24807  iscmet3lem3  24814  cfilresi  24819  causs  24822  lmclim  24827  ivth2  24979  ovolfioo  24991  ovolficc  24992  ovolshftlem1  25033  ovolscalem1  25037  volsup2  25129  ismbf3d  25178  mbfaddlem  25184  mbfsup  25188  mbfinf  25189  itg2seq  25267  itg2gt0  25285  ellimc2  25401  ellimc3  25403  rolle  25514  cmvth  25515  mvth  25516  dvlip  25517  dvivth  25534  lhop1lem  25537  deg1ldg  25617  ulm2  25904  ulmdvlem3  25921  dcubic  26358  mcubic  26359  cubic2  26360  rlimcnp  26477  ftalem3  26586  isppw2  26626  lgsquadlem2  26891  2lgslem1a  26901  dchrmusumlema  27003  dchrisum0lema  27024  cofcutr  27420  lrrecfr  27436  addsrid  27457  addscom  27459  addsuniflem  27494  addsass  27498  negsunif  27539  mulsrid  27579  mulsasslem3  27630  tglowdim2l  27939  mirreu3  27943  oppcom  28033  iscgra1  28099  axsegcon  28223  axpasch  28237  axcontlem7  28266  usgr2pth0  29060  usgr2wspthon  29257  elwwlks2  29258  elwspths2spth  29259  rusgrnumwwlks  29266  clwwlkfo  29341  eclclwwlkn1  29366  eucrctshift  29534  fusgreg2wsp  29627  nmobndi  30066  nmounbi  30067  nmoo0  30082  h2hcau  30270  h2hlm  30271  shsel3  30606  pjhtheu2  30707  chscllem2  30929  adjbdln  31374  branmfn  31396  pjimai  31467  chrelati  31655  cdj3lem3  31729  cdj3lem3b  31731  dfimafnf  31898  ofpreima  31928  isarchi2  32372  submarchi  32373  archirng  32375  archiabl  32385  isarchiofld  32476  ellspds  32526  lsmssass  32557  grplsm0l  32558  fedgmullem2  32774  elirng  32810  zarcls  32923  ordtconnlem1  32973  lmdvg  33002  esumfsup  33137  dya2icoseg2  33346  eulerpartlemgh  33446  ballotlemodife  33565  ballotlemsima  33583  nummin  34163  erdszelem10  34260  iscvm  34319  wsuclem  34866  seglelin  35157  outsideofeu  35172  gg-cmvth  35250  opnrebl  35291  opnrebl2  35292  filnetlem4  35352  bj-finsumval0  36252  phpreu  36558  ptrest  36573  poimirlem3  36577  poimirlem4  36578  poimirlem17  36591  poimirlem26  36600  poimirlem27  36601  broucube  36608  mblfinlem1  36611  lmclim2  36712  caures  36714  isbnd3b  36739  heiborlem7  36771  heiborlem10  36774  rrncmslem  36786  isdrngo2  36912  erimeq2  37634  prter3  37838  islshpsm  37936  lsatfixedN  37965  lrelat  37970  eqlkr2  38056  lshpkrlem1  38066  lfl1dim  38077  eqlkr4  38121  ishlat3N  38310  hlsupr2  38344  hlrelat5N  38358  hlrelat  38359  cvrval5  38372  cvrat42  38401  athgt  38413  3dim0  38414  islln3  38467  llnexatN  38478  islpln3  38490  islvol3  38533  islvol5  38536  isline4N  38734  polval2N  38863  4atex3  39038  cdleme0ex2N  39181  cdlemefrs29cpre1  39355  cdlemb3  39563  cdlemg33c  39665  cdlemg33e  39667  dia1dim2  40019  cdlemm10N  40075  dib1dim2  40125  diclspsn  40151  dih1dimatlem  40286  dihatexv2  40296  djhcvat42  40372  dihjat1lem  40385  dvh4dimat  40395  dvh2dimatN  40397  lcfrlem9  40507  mapdval4N  40589  mapdcv  40617  infdesc  41467  elrfirn  41515  elrfirn2  41516  mrefg3  41528  diophin  41592  diophun  41593  diophren  41633  rmxycomplete  41738  wepwsolem  41866  fnwe2lem2  41875  islssfg  41894  unielss  42049  onmaxnelsup  42054  onsupnmax  42059  onsupeqnmax  42078  tfsconcat0i  42177  ntrneineine0lem  42916  ntrneineine1lem  42917  ntrneiel2  42919  extoimad  42998  grumnudlem  43126  supsubc  44142  infxrbnd2  44158  supminfxr  44253  evthiccabs  44288  elicores  44325  clim2f  44431  clim2cf  44445  clim0cf  44449  clim2f2  44465  limsupub  44499  limsupmnflem  44515  limsupre2lem  44519  limsuplt2  44548  liminfreuzlem  44597  liminfltlem  44599  liminflimsupclim  44602  xlimmnfmpt  44638  xlimpnfmpt  44639  fourierdlem73  44974  fourierdlem83  44984  meaiuninc3v  45279  ovolval2  45439  cfsetsnfsetfo  45849  dfaimafn  45952  iccelpart  46180  sprsymrelf  46242  sprsymrelfo  46244  fmtnoprmfac1  46312  fmtnoprmfac2  46314  fmtnofac2lem  46315  dfeven2  46396  dfodd3  46397  isomuspgrlem2d  46578  uspgrsprfo  46605  rngqiprngimfo  46865  pzriprnglem10  46893  elbigo2  47316  rrxlinesc  47499  rrxlinec  47500  rrx2line  47504  rrx2vlinest  47505  itsclquadeu  47541