Theorem rexbidva 3158

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

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

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 3061

This theorem is referenced by:  rexbidv  3160  2rexbiia  3197  2rexbidva  3199  rexeqbidva  3303  frinxp  5707  onfr  6356  dfimafn  6896  funimass4  6898  fliftel  7255  fliftf  7261  isomin  7283  f1oiso  7297  releldm2  7987  oaass  8488  eldifsucnn  8592  cofonr  8602  naddunif  8621  qsinxp  8730  qliftel  8737  fimaxg  9187  ordunifi  9190  supisolem  9377  fiming  9403  wemapwe  9606  ttrcltr  9625  ttrclse  9636  frmin  9661  cflim2  10173  cfsmolem  10180  alephsing  10186  brdom7disj  10441  brdom6disj  10442  alephreg  10493  nqereu  10840  1idpr  10940  map2psrpr  11021  axsup  11208  rereccl  11859  sup3  12099  infm3  12101  supadd  12110  creur  12139  creui  12140  nndiv  12191  nnrecl  12399  rpnnen1lem2  12890  rpnnen1lem1  12891  rpnnen1lem3  12892  rpnnen1lem5  12894  supxrbnd1  13236  supxrbnd2  13237  supxrbnd  13243  rabssnn0fi  13909  mptnn0fsupp  13920  expnlbnd  14156  wrdl3s3  14885  limsuplt  15402  clim2  15427  clim2c  15428  clim0c  15430  ello12  15439  elo12  15450  rlimresb  15488  climabs0  15508  sumeq2ii  15616  mertens  15809  prodeq2ii  15834  zprod  15860  nndivides  16189  alzdvds  16247  oddm1even  16270  oddnn02np1  16275  oddge22np1  16276  evennn02n  16277  evennn2n  16278  divalglem4  16323  divalgb  16331  modremain  16335  modprmn0modprm0  16735  vdwlem6  16914  vdwlem11  16919  vdw  16922  ramval  16936  imasleval  17462  dfiso3  17697  fullestrcsetc  18074  fullsetcestrc  18089  isipodrs  18460  ipodrsfi  18462  gsumpropd2lem  18604  mndpropd  18684  grppropd  18881  qus0subgbas  19127  conjnmzb  19182  symgextfo  19351  symgfixfo  19368  sylow1lem2  19528  sylow3lem1  19556  sylow3lem3  19558  lsmelvalm  19580  lsmass  19598  iscyg3  19815  ghmcyg  19825  cycsubgcyg  19830  pgpfac1lem2  20006  pgpfac1lem4  20009  ablfac2  20020  dvdsr02  20308  crngunit  20314  dvdsrpropd  20352  rngqiprngimfo  21256  lpigen  21290  pzriprnglem10  21445  znunit  21518  elfilspd  21758  psdmul  22109  scmatmats  22455  symgmatr01  22598  isclo  23031  iscnp3  23188  lmbrf  23204  cncnp  23224  lmss  23242  isnrm2  23302  cmpfi  23352  1stcfb  23389  1stccnp  23406  ptrescn  23583  txkgen  23596  xkoinjcn  23631  trfil3  23832  fmid  23904  lmflf  23949  txflf  23950  ptcmplem3  23998  tsmsf1o  24089  ucnprima  24225  metrest  24468  metcnp  24485  metcnp2  24486  txmetcnp  24491  metuel2  24509  metustbl  24510  psmetutop  24511  metucn  24515  evth2  24915  lmmbrf  25218  iscfil2  25222  fmcfil  25228  iscau2  25233  iscau4  25235  iscauf  25236  caucfil  25239  iscmet3lem3  25246  cfilresi  25251  causs  25254  lmclim  25259  ivth2  25412  ovolfioo  25424  ovolficc  25425  ovolshftlem1  25466  ovolscalem1  25470  volsup2  25562  ismbf3d  25611  mbfaddlem  25617  mbfsup  25621  mbfinf  25622  itg2seq  25699  itg2gt0  25717  ellimc2  25834  ellimc3  25836  rolle  25950  cmvth  25951  cmvthOLD  25952  mvth  25953  dvlip  25954  dvivth  25971  lhop1lem  25974  deg1ldg  26053  ulm2  26350  ulmdvlem3  26367  dcubic  26812  mcubic  26813  cubic2  26814  rlimcnp  26931  ftalem3  27041  isppw2  27081  lgsquadlem2  27348  2lgslem1a  27358  dchrmusumlema  27460  dchrisum0lema  27481  cofcutr  27920  lrrecfr  27939  addsrid  27960  addscom  27962  addsuniflem  27997  addsass  28001  addbday  28014  negsunif  28051  mulsrid  28109  mulsasslem3  28161  n0s0suc  28338  z12sge0  28479  elreno2  28491  renegscl  28494  readdscl  28495  remulscllem2  28497  remulscl  28498  tglowdim2l  28722  mirreu3  28726  oppcom  28816  iscgra1  28882  axsegcon  29000  axpasch  29014  axcontlem7  29043  usgr2pth0  29838  usgr2wspthon  30041  elwwlks2  30042  elwspths2spth  30043  rusgrnumwwlks  30050  clwwlkfo  30125  eclclwwlkn1  30150  eucrctshift  30318  fusgreg2wsp  30411  nmobndi  30850  nmounbi  30851  nmoo0  30866  h2hcau  31054  h2hlm  31055  shsel3  31390  pjhtheu2  31491  chscllem2  31713  adjbdln  32158  branmfn  32180  pjimai  32251  chrelati  32439  cdj3lem3  32513  cdj3lem3b  32515  dfimafnf  32714  ofpreima  32743  isarchi2  33267  submarchi  33268  archirng  33270  archiabl  33280  isarchiofld  33281  ellspds  33449  dvdsruasso2  33467  lsmssass  33483  grplsm0l  33484  fedgmullem2  33787  elirng  33843  zarcls  34031  ordtconnlem1  34081  lmdvg  34110  esumfsup  34227  dya2icoseg2  34435  eulerpartlemgh  34535  ballotlemodife  34655  ballotlemsima  34673  nummin  35249  erdszelem10  35394  iscvm  35453  wsuclem  36017  seglelin  36310  outsideofeu  36325  opnrebl  36514  opnrebl2  36515  filnetlem4  36575  bj-finsumval0  37490  phpreu  37805  ptrest  37820  poimirlem3  37824  poimirlem4  37825  poimirlem17  37838  poimirlem26  37847  poimirlem27  37848  broucube  37855  mblfinlem1  37858  lmclim2  37959  caures  37961  isbnd3b  37986  heiborlem7  38018  heiborlem10  38021  rrncmslem  38033  isdrngo2  38159  erimeq2  38937  prter3  39142  islshpsm  39240  lsatfixedN  39269  lrelat  39274  eqlkr2  39360  lshpkrlem1  39370  lfl1dim  39381  eqlkr4  39425  ishlat3N  39614  hlsupr2  39647  hlrelat5N  39661  hlrelat  39662  cvrval5  39675  cvrat42  39704  athgt  39716  3dim0  39717  islln3  39770  llnexatN  39781  islpln3  39793  islvol3  39836  islvol5  39839  isline4N  40037  polval2N  40166  4atex3  40341  cdleme0ex2N  40484  cdlemefrs29cpre1  40658  cdlemb3  40866  cdlemg33c  40968  cdlemg33e  40970  dia1dim2  41322  cdlemm10N  41378  dib1dim2  41428  diclspsn  41454  dih1dimatlem  41589  dihatexv2  41599  djhcvat42  41675  dihjat1lem  41688  dvh4dimat  41698  dvh2dimatN  41700  lcfrlem9  41810  mapdval4N  41892  mapdcv  41920  ef11d  42594  cxp112d  42596  cxp111d  42597  sn-sup3d  42747  fimgmcyc  42789  infdesc  42886  elrfirn  42937  elrfirn2  42938  mrefg3  42950  diophin  43014  diophun  43015  diophren  43055  rmxycomplete  43159  wepwsolem  43284  fnwe2lem2  43293  islssfg  43312  unielss  43460  onmaxnelsup  43465  onsupnmax  43470  onsupeqnmax  43489  tfsconcat0i  43587  ntrneineine0lem  44324  ntrneineine1lem  44325  ntrneiel2  44327  extoimad  44405  grumnudlem  44526  modelac8prim  45233  supsubc  45598  infxrbnd2  45613  supminfxr  45708  evthiccabs  45742  elicores  45779  clim2f  45880  clim2cf  45894  clim0cf  45898  clim2f2  45914  limsupub  45948  limsupmnflem  45964  limsupre2lem  45968  limsuplt2  45997  liminfreuzlem  46046  liminfltlem  46048  liminflimsupclim  46051  xlimmnfmpt  46087  xlimpnfmpt  46088  fourierdlem73  46423  fourierdlem83  46433  meaiuninc3v  46728  ovolval2  46888  cfsetsnfsetfo  47306  dfaimafn  47411  iccelpart  47679  sprsymrelf  47741  sprsymrelfo  47743  fmtnoprmfac1  47811  fmtnoprmfac2  47813  fmtnofac2lem  47814  dfeven2  47895  dfodd3  47896  dfvopnbgr2  48099  usgrgrtrirex  48196  stgredgiun  48204  uspgrsprfo  48394  elbigo2  48798  rrxlinesc  48981  rrxlinec  48982  rrx2line  48986  rrx2vlinest  48987  itsclquadeu  49023