Theorem rexbidva 3185

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  ∃wrex 3087

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

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

This theorem is used by:  rexbidv  3187  2rexbiia  3224  2rexbidva  3226  rexeqbidva  3327  frinxp  5734  onfr  6401  dfimafn  6945  funimass4  6947  fliftel  7315  fliftf  7321  isomin  7343  f1oiso  7357  releldm2  8052  oaass  8562  eldifsucnn  8666  cofonr  8676  naddunif  8696  qsinxp  8807  qliftel  8814  fimaxg  9271  ordunifi  9274  supisolem  9459  fiming  9485  wemapwe  9691  ttrcltr  9710  ttrclse  9721  frmin  9746  cflim2  10334  cfsmolem  10341  alephsing  10347  brdom7disj  10603  brdom6disj  10604  alephreg  10660  nqereu  11007  1idpr  11107  map2psrpr  11188  axsup  11378  rereccl  12028  sup3  12267  infm3  12269  supadd  12278  creur  12307  creui  12308  nndiv  12377  nnrecl  12597  rpnnen1lem2  13098  rpnnen1lem1  13099  rpnnen1lem3  13100  rpnnen1lem5  13102  supxrbnd1  13444  supxrbnd2  13445  supxrbnd  13451  rabssnn0fi  14122  mptnn0fsupp  14133  expnlbnd  14370  wrdl3s3  15108  limsuplt  15639  clim2  15664  clim2c  15665  clim0c  15667  ello12  15676  elo12  15687  rlimresb  15725  climabs0  15745  sumeq2ii  15853  mertens  16048  prodeq2ii  16073  zprod  16097  nndivides  16425  alzdvds  16483  oddm1even  16506  oddnn02np1  16511  oddge22np1  16512  evennn02n  16513  evennn2n  16514  divalglem4  16559  divalgb  16567  modremain  16571  modprmn0modprm0  16978  vdwlem6  17157  vdwlem11  17162  vdw  17165  ramval  17179  imasleval  17706  dfiso3  17941  fullestrcsetc  18318  fullsetcestrc  18333  isipodrs  18704  ipodrsfi  18706  mgmidpfod  18850  gsumpropd2lem  18861  mndpropd  18944  grppropd  19155  qus0subgbas  19406  conjnmzb  19460  symgextfo  19629  symgfixfo  19646  sylow1lem2  19806  sylow3lem1  19834  sylow3lem3  19836  lsmelvalm  19858  lsmass  19876  iscyg3  20093  ghmcyg  20103  cycsubgcyg  20108  pgpfac1lem2  20284  pgpfac1lem4  20287  ablfac2  20298  dvdsr02  20595  crngunit  20601  dvdsrpropd  20639  rngqiprngimfo  21590  lpigen  21652  pzriprnglem10  21789  znunit  21862  elfilspd  22102  psdmul  22480  scmatmats  22819  symgmatr01  22962  isclo  23398  iscnp3  23555  lmbrf  23571  cncnp  23591  lmss  23609  isnrm2  23669  cmpfi  23719  1stcfb  23756  1stccnp  23774  ptrescn  23951  txkgen  23964  xkoinjcn  23999  trfil3  24200  fmid  24272  lmflf  24317  txflf  24318  ptcmplem3  24366  tsmsf1o  24457  ucnprima  24593  metrest  24836  metcnp  24853  metcnp2  24854  txmetcnp  24859  metuel2  24877  metustbl  24878  psmetutop  24879  metucn  24883  evth2  25274  lmmbrf  25576  iscfil2  25580  fmcfil  25586  iscau2  25591  iscau4  25593  iscauf  25594  caucfil  25597  iscmet3lem3  25604  cfilresi  25609  causs  25612  lmclim  25617  ivth2  25769  ovolfioo  25781  ovolficc  25782  ovolshftlem1  25823  ovolscalem1  25827  volsup2  25919  ismbf3d  25968  mbfaddlem  25974  mbfsup  25978  mbfinf  25979  itg2seq  26056  itg2gt0  26074  ellimc2  26190  ellimc3  26192  rolle  26303  cmvth  26304  mvth  26305  dvlip  26306  dvivth  26323  lhop1lem  26326  deg1ldg  26403  rnplynfin  26623  plyconz  26624  ulm2  26705  ulmdvlem3  26722  dcubic  27167  mcubic  27168  cubic2  27169  rlimcnp  27286  ftalem3  27395  isppw2  27435  lgsquadlem2  27701  2lgslem1a  27711  dchrmusumlema  27813  dchrisum0lema  27834  infdesc  27960  cofcutr  28303  lrrecfr  28322  addsrid  28343  addscom  28345  addsuniflem  28380  addsass  28384  addbday  28397  negsunif  28434  mulsrid  28492  mulsasslem3  28544  n0s0suc  28721  z12sge0  28862  elreno2  28874  renegscl  28877  readdscl  28878  remulscllem2  28880  remulscl  28881  tglowdim2l  29112  mirreu3  29119  oppcom  29213  iscgra1  29310  axsegcon  29498  axpasch  29512  axcontlem7  29541  usgr2pth0  30344  usgr2wspthon  30550  elwwlks2  30551  elwspths2spth  30552  rusgrnumwwlks  30559  clwwlkfo  30634  eclclwwlkn1  30659  eucrctshift  30837  fusgreg2wsp  30930  nmobndi  31370  nmounbi  31371  nmoo0  31386  h2hcau  31574  h2hlm  31575  shsel3  31910  pjhtheu2  32011  chscllem2  32233  adjbdln  32678  branmfn  32700  pjimai  32771  chrelati  32959  cdj3lem3  33033  cdj3lem3b  33035  dfimafnf  33223  ofpreima  33252  isarchi2  33739  submarchi  33740  archirng  33742  archiabl  33752  isarchiofld  33753  isunitc  33795  ellspds  33917  dvdsruasso2  33934  lsmssass  33946  grplsm0l  33947  fedgmullem2  34255  elirng  34311  zarcls  34499  ordtconnlem1  34549  lmdvg  34578  esumfsup  34695  dya2icoseg2  34903  eulerpartlemgh  35003  ballotlemodife  35123  ballotlemsima  35141  nummin  35711  erdszelem10  35944  iscvm  36003  wsuclem  36567  seglelin  36861  outsideofeu  36876  ltnadd  36947  naddle  36948  opnrebl  37088  opnrebl2  37089  filnetlem4  37149  bj-finsumval0  38186  phpreu  38507  ptrest  38517  poimirlem3  38521  poimirlem4  38522  poimirlem17  38535  poimirlem26  38544  poimirlem27  38545  broucube  38552  mblfinlem1  38555  lmclim2  38672  caures  38674  isbnd3b  38699  heiborlem7  38731  heiborlem10  38734  rrncmslem  38746  isdrngo2  38872  erimeq2  39675  prter3  39919  islshpsm  40017  lsatfixedN  40046  lrelat  40051  eqlkr2  40137  lshpkrlem1  40147  lfl1dim  40158  eqlkr4  40202  ishlat3N  40391  hlsupr2  40424  hlrelat5N  40438  hlrelat  40439  cvrval5  40452  cvrat42  40481  athgt  40493  3dim0  40494  islln3  40547  llnexatN  40558  islpln3  40570  islvol3  40613  islvol5  40616  isline4N  40814  polval2N  40943  4atex3  41118  cdleme0ex2N  41261  cdlemefrs29cpre1  41435  cdlemb3  41643  cdlemg33c  41745  cdlemg33e  41747  dia1dim2  42099  cdlemm10N  42155  dib1dim2  42205  diclspsn  42231  dih1dimatlem  42366  dihatexv2  42376  djhcvat42  42452  dihjat1lem  42465  dvh4dimat  42475  dvh2dimatN  42477  lcfrlem9  42587  mapdval4N  42669  mapdcv  42697  ef11d  43370  cxp112d  43372  cxp111d  43373  sn-sup3d  43536  fimgmcyc  43578  elrfirn  43685  elrfirn2  43686  mrefg3  43698  diophin  43762  diophun  43763  diophren  43799  rmxycomplete  43903  wepwsolem  44028  fnwe2lem2  44037  islssfg  44056  unielss  44204  onmaxnelsup  44209  onsupnmax  44214  onsupeqnmax  44233  tfsconcat0i  44331  ntrneineine0lem  45068  ntrneineine1lem  45069  ntrneiel2  45071  extoimad  45149  grumnudlem  45254  modelac8prim  45960  supsubc  46334  infxrbnd2  46349  supminfxr  46443  evthiccabs  46477  elicores  46514  clim2f  46615  clim2cf  46629  clim0cf  46633  clim2f2  46649  limsupub  46683  limsupmnflem  46699  limsupre2lem  46703  limsuplt2  46732  liminfreuzlem  46781  liminfltlem  46783  liminflimsupclim  46786  xlimmnfmpt  46822  xlimpnfmpt  46823  fourierdlem73  47158  fourierdlem83  47168  meaiuninc3v  47463  ovolval2  47623  cfsetsnfsetfo  48099  dfaimafn  48204  iccelpart  48484  sprsymrelf  48546  sprsymrelfo  48548  nprmmul1  48578  nprmmul3  48580  fmtnoprmfac1  48619  fmtnoprmfac2  48621  fmtnofac2lem  48622  dfeven2  48716  dfodd3  48717  dfvopnbgr2  48920  usgrgrtrirex  49017  stgredgiun  49025  uspgrsprfo  49215  elbigo2  49633  rrxlinesc  49816  rrxlinec  49817  rrx2line  49821  rrx2vlinest  49822  itsclquadeu  49858