Theorem rexbidva 3156

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2113  ∃wrex 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3059

This theorem is referenced by:  rexbidv  3158  2rexbiia  3195  2rexbidva  3197  rexeqbidva  3301  frinxp  5705  onfr  6354  dfimafn  6894  funimass4  6896  fliftel  7253  fliftf  7259  isomin  7281  f1oiso  7295  releldm2  7985  oaass  8486  eldifsucnn  8590  cofonr  8600  naddunif  8619  qsinxp  8728  qliftel  8735  fimaxg  9185  ordunifi  9188  supisolem  9375  fiming  9401  wemapwe  9604  ttrcltr  9623  ttrclse  9634  frmin  9659  cflim2  10171  cfsmolem  10178  alephsing  10184  brdom7disj  10439  brdom6disj  10440  alephreg  10491  nqereu  10838  1idpr  10938  map2psrpr  11019  axsup  11206  rereccl  11857  sup3  12097  infm3  12099  supadd  12108  creur  12137  creui  12138  nndiv  12189  nnrecl  12397  rpnnen1lem2  12888  rpnnen1lem1  12889  rpnnen1lem3  12890  rpnnen1lem5  12892  supxrbnd1  13234  supxrbnd2  13235  supxrbnd  13241  rabssnn0fi  13907  mptnn0fsupp  13918  expnlbnd  14154  wrdl3s3  14883  limsuplt  15400  clim2  15425  clim2c  15426  clim0c  15428  ello12  15437  elo12  15448  rlimresb  15486  climabs0  15506  sumeq2ii  15614  mertens  15807  prodeq2ii  15832  zprod  15858  nndivides  16187  alzdvds  16245  oddm1even  16268  oddnn02np1  16273  oddge22np1  16274  evennn02n  16275  evennn2n  16276  divalglem4  16321  divalgb  16329  modremain  16333  modprmn0modprm0  16733  vdwlem6  16912  vdwlem11  16917  vdw  16920  ramval  16934  imasleval  17460  dfiso3  17695  fullestrcsetc  18072  fullsetcestrc  18087  isipodrs  18458  ipodrsfi  18460  gsumpropd2lem  18602  mndpropd  18682  grppropd  18879  qus0subgbas  19125  conjnmzb  19180  symgextfo  19349  symgfixfo  19366  sylow1lem2  19526  sylow3lem1  19554  sylow3lem3  19556  lsmelvalm  19578  lsmass  19596  iscyg3  19813  ghmcyg  19823  cycsubgcyg  19828  pgpfac1lem2  20004  pgpfac1lem4  20007  ablfac2  20018  dvdsr02  20306  crngunit  20312  dvdsrpropd  20350  rngqiprngimfo  21254  lpigen  21288  pzriprnglem10  21443  znunit  21516  elfilspd  21756  psdmul  22107  scmatmats  22453  symgmatr01  22596  isclo  23029  iscnp3  23186  lmbrf  23202  cncnp  23222  lmss  23240  isnrm2  23300  cmpfi  23350  1stcfb  23387  1stccnp  23404  ptrescn  23581  txkgen  23594  xkoinjcn  23629  trfil3  23830  fmid  23902  lmflf  23947  txflf  23948  ptcmplem3  23996  tsmsf1o  24087  ucnprima  24223  metrest  24466  metcnp  24483  metcnp2  24484  txmetcnp  24489  metuel2  24507  metustbl  24508  psmetutop  24509  metucn  24513  evth2  24913  lmmbrf  25216  iscfil2  25220  fmcfil  25226  iscau2  25231  iscau4  25233  iscauf  25234  caucfil  25237  iscmet3lem3  25244  cfilresi  25249  causs  25252  lmclim  25257  ivth2  25410  ovolfioo  25422  ovolficc  25423  ovolshftlem1  25464  ovolscalem1  25468  volsup2  25560  ismbf3d  25609  mbfaddlem  25615  mbfsup  25619  mbfinf  25620  itg2seq  25697  itg2gt0  25715  ellimc2  25832  ellimc3  25834  rolle  25948  cmvth  25949  cmvthOLD  25950  mvth  25951  dvlip  25952  dvivth  25969  lhop1lem  25972  deg1ldg  26051  ulm2  26348  ulmdvlem3  26365  dcubic  26810  mcubic  26811  cubic2  26812  rlimcnp  26929  ftalem3  27039  isppw2  27079  lgsquadlem2  27346  2lgslem1a  27356  dchrmusumlema  27458  dchrisum0lema  27479  cofcutr  27895  lrrecfr  27913  addsrid  27934  addscom  27936  addsuniflem  27971  addsass  27975  addsbday  27987  negsunif  28024  mulsrid  28082  mulsasslem3  28134  n0s0suc  28302  zs12ge0  28432  elreno2  28440  renegscl  28443  readdscl  28444  remulscllem2  28446  remulscl  28447  tglowdim2l  28671  mirreu3  28675  oppcom  28765  iscgra1  28831  axsegcon  28949  axpasch  28963  axcontlem7  28992  usgr2pth0  29787  usgr2wspthon  29990  elwwlks2  29991  elwspths2spth  29992  rusgrnumwwlks  29999  clwwlkfo  30074  eclclwwlkn1  30099  eucrctshift  30267  fusgreg2wsp  30360  nmobndi  30799  nmounbi  30800  nmoo0  30815  h2hcau  31003  h2hlm  31004  shsel3  31339  pjhtheu2  31440  chscllem2  31662  adjbdln  32107  branmfn  32129  pjimai  32200  chrelati  32388  cdj3lem3  32462  cdj3lem3b  32464  dfimafnf  32663  ofpreima  32692  isarchi2  33216  submarchi  33217  archirng  33219  archiabl  33229  isarchiofld  33230  ellspds  33398  dvdsruasso2  33416  lsmssass  33432  grplsm0l  33433  fedgmullem2  33736  elirng  33792  zarcls  33980  ordtconnlem1  34030  lmdvg  34059  esumfsup  34176  dya2icoseg2  34384  eulerpartlemgh  34484  ballotlemodife  34604  ballotlemsima  34622  nummin  35198  erdszelem10  35343  iscvm  35402  wsuclem  35966  seglelin  36259  outsideofeu  36274  opnrebl  36463  opnrebl2  36464  filnetlem4  36524  bj-finsumval0  37429  phpreu  37744  ptrest  37759  poimirlem3  37763  poimirlem4  37764  poimirlem17  37777  poimirlem26  37786  poimirlem27  37787  broucube  37794  mblfinlem1  37797  lmclim2  37898  caures  37900  isbnd3b  37925  heiborlem7  37957  heiborlem10  37960  rrncmslem  37972  isdrngo2  38098  erimeq2  38876  prter3  39081  islshpsm  39179  lsatfixedN  39208  lrelat  39213  eqlkr2  39299  lshpkrlem1  39309  lfl1dim  39320  eqlkr4  39364  ishlat3N  39553  hlsupr2  39586  hlrelat5N  39600  hlrelat  39601  cvrval5  39614  cvrat42  39643  athgt  39655  3dim0  39656  islln3  39709  llnexatN  39720  islpln3  39732  islvol3  39775  islvol5  39778  isline4N  39976  polval2N  40105  4atex3  40280  cdleme0ex2N  40423  cdlemefrs29cpre1  40597  cdlemb3  40805  cdlemg33c  40907  cdlemg33e  40909  dia1dim2  41261  cdlemm10N  41317  dib1dim2  41367  diclspsn  41393  dih1dimatlem  41528  dihatexv2  41538  djhcvat42  41614  dihjat1lem  41627  dvh4dimat  41637  dvh2dimatN  41639  lcfrlem9  41749  mapdval4N  41831  mapdcv  41859  ef11d  42536  cxp112d  42538  cxp111d  42539  sn-sup3d  42689  fimgmcyc  42731  infdesc  42828  elrfirn  42879  elrfirn2  42880  mrefg3  42892  diophin  42956  diophun  42957  diophren  42997  rmxycomplete  43101  wepwsolem  43226  fnwe2lem2  43235  islssfg  43254  unielss  43402  onmaxnelsup  43407  onsupnmax  43412  onsupeqnmax  43431  tfsconcat0i  43529  ntrneineine0lem  44266  ntrneineine1lem  44267  ntrneiel2  44269  extoimad  44347  grumnudlem  44468  modelac8prim  45175  supsubc  45540  infxrbnd2  45555  supminfxr  45650  evthiccabs  45684  elicores  45721  clim2f  45822  clim2cf  45836  clim0cf  45840  clim2f2  45856  limsupub  45890  limsupmnflem  45906  limsupre2lem  45910  limsuplt2  45939  liminfreuzlem  45988  liminfltlem  45990  liminflimsupclim  45993  xlimmnfmpt  46029  xlimpnfmpt  46030  fourierdlem73  46365  fourierdlem83  46375  meaiuninc3v  46670  ovolval2  46830  cfsetsnfsetfo  47248  dfaimafn  47353  iccelpart  47621  sprsymrelf  47683  sprsymrelfo  47685  fmtnoprmfac1  47753  fmtnoprmfac2  47755  fmtnofac2lem  47756  dfeven2  47837  dfodd3  47838  dfvopnbgr2  48041  usgrgrtrirex  48138  stgredgiun  48146  uspgrsprfo  48336  elbigo2  48740  rrxlinesc  48923  rrxlinec  48924  rrx2line  48928  rrx2vlinest  48929  itsclquadeu  48965