Theorem rexbidva 3160

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

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

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 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  rexbidv  3162  2rexbiia  3199  2rexbidva  3201  rexeqbidva  3305  frinxp  5715  onfr  6364  dfimafn  6904  funimass4  6906  fliftel  7265  fliftf  7271  isomin  7293  f1oiso  7307  releldm2  7997  oaass  8498  eldifsucnn  8602  cofonr  8612  naddunif  8631  qsinxp  8742  qliftel  8749  fimaxg  9199  ordunifi  9202  supisolem  9389  fiming  9415  wemapwe  9618  ttrcltr  9637  ttrclse  9648  frmin  9673  cflim2  10185  cfsmolem  10192  alephsing  10198  brdom7disj  10453  brdom6disj  10454  alephreg  10505  nqereu  10852  1idpr  10952  map2psrpr  11033  axsup  11220  rereccl  11871  sup3  12111  infm3  12113  supadd  12122  creur  12151  creui  12152  nndiv  12203  nnrecl  12411  rpnnen1lem2  12902  rpnnen1lem1  12903  rpnnen1lem3  12904  rpnnen1lem5  12906  supxrbnd1  13248  supxrbnd2  13249  supxrbnd  13255  rabssnn0fi  13921  mptnn0fsupp  13932  expnlbnd  14168  wrdl3s3  14897  limsuplt  15414  clim2  15439  clim2c  15440  clim0c  15442  ello12  15451  elo12  15462  rlimresb  15500  climabs0  15520  sumeq2ii  15628  mertens  15821  prodeq2ii  15846  zprod  15872  nndivides  16201  alzdvds  16259  oddm1even  16282  oddnn02np1  16287  oddge22np1  16288  evennn02n  16289  evennn2n  16290  divalglem4  16335  divalgb  16343  modremain  16347  modprmn0modprm0  16747  vdwlem6  16926  vdwlem11  16931  vdw  16934  ramval  16948  imasleval  17474  dfiso3  17709  fullestrcsetc  18086  fullsetcestrc  18101  isipodrs  18472  ipodrsfi  18474  gsumpropd2lem  18616  mndpropd  18696  grppropd  18893  qus0subgbas  19139  conjnmzb  19194  symgextfo  19363  symgfixfo  19380  sylow1lem2  19540  sylow3lem1  19568  sylow3lem3  19570  lsmelvalm  19592  lsmass  19610  iscyg3  19827  ghmcyg  19837  cycsubgcyg  19842  pgpfac1lem2  20018  pgpfac1lem4  20021  ablfac2  20032  dvdsr02  20320  crngunit  20326  dvdsrpropd  20364  rngqiprngimfo  21268  lpigen  21302  pzriprnglem10  21457  znunit  21530  elfilspd  21770  psdmul  22121  scmatmats  22467  symgmatr01  22610  isclo  23043  iscnp3  23200  lmbrf  23216  cncnp  23236  lmss  23254  isnrm2  23314  cmpfi  23364  1stcfb  23401  1stccnp  23418  ptrescn  23595  txkgen  23608  xkoinjcn  23643  trfil3  23844  fmid  23916  lmflf  23961  txflf  23962  ptcmplem3  24010  tsmsf1o  24101  ucnprima  24237  metrest  24480  metcnp  24497  metcnp2  24498  txmetcnp  24503  metuel2  24521  metustbl  24522  psmetutop  24523  metucn  24527  evth2  24927  lmmbrf  25230  iscfil2  25234  fmcfil  25240  iscau2  25245  iscau4  25247  iscauf  25248  caucfil  25251  iscmet3lem3  25258  cfilresi  25263  causs  25266  lmclim  25271  ivth2  25424  ovolfioo  25436  ovolficc  25437  ovolshftlem1  25478  ovolscalem1  25482  volsup2  25574  ismbf3d  25623  mbfaddlem  25629  mbfsup  25633  mbfinf  25634  itg2seq  25711  itg2gt0  25729  ellimc2  25846  ellimc3  25848  rolle  25962  cmvth  25963  cmvthOLD  25964  mvth  25965  dvlip  25966  dvivth  25983  lhop1lem  25986  deg1ldg  26065  ulm2  26362  ulmdvlem3  26379  dcubic  26824  mcubic  26825  cubic2  26826  rlimcnp  26943  ftalem3  27053  isppw2  27093  lgsquadlem2  27360  2lgslem1a  27370  dchrmusumlema  27472  dchrisum0lema  27493  cofcutr  27932  lrrecfr  27951  addsrid  27972  addscom  27974  addsuniflem  28009  addsass  28013  addbday  28026  negsunif  28063  mulsrid  28121  mulsasslem3  28173  n0s0suc  28350  z12sge0  28491  elreno2  28503  renegscl  28506  readdscl  28507  remulscllem2  28509  remulscl  28510  tglowdim2l  28734  mirreu3  28738  oppcom  28828  iscgra1  28894  axsegcon  29012  axpasch  29026  axcontlem7  29055  usgr2pth0  29850  usgr2wspthon  30053  elwwlks2  30054  elwspths2spth  30055  rusgrnumwwlks  30062  clwwlkfo  30137  eclclwwlkn1  30162  eucrctshift  30330  fusgreg2wsp  30423  nmobndi  30863  nmounbi  30864  nmoo0  30879  h2hcau  31067  h2hlm  31068  shsel3  31403  pjhtheu2  31504  chscllem2  31726  adjbdln  32171  branmfn  32193  pjimai  32264  chrelati  32452  cdj3lem3  32526  cdj3lem3b  32528  dfimafnf  32726  ofpreima  32755  isarchi2  33279  submarchi  33280  archirng  33282  archiabl  33292  isarchiofld  33293  ellspds  33461  dvdsruasso2  33479  lsmssass  33495  grplsm0l  33496  fedgmullem2  33808  elirng  33864  zarcls  34052  ordtconnlem1  34102  lmdvg  34131  esumfsup  34248  dya2icoseg2  34456  eulerpartlemgh  34556  ballotlemodife  34676  ballotlemsima  34694  nummin  35270  erdszelem10  35416  iscvm  35475  wsuclem  36039  seglelin  36332  outsideofeu  36347  opnrebl  36536  opnrebl2  36537  filnetlem4  36597  bj-finsumval0  37540  phpreu  37855  ptrest  37870  poimirlem3  37874  poimirlem4  37875  poimirlem17  37888  poimirlem26  37897  poimirlem27  37898  broucube  37905  mblfinlem1  37908  lmclim2  38009  caures  38011  isbnd3b  38036  heiborlem7  38068  heiborlem10  38071  rrncmslem  38083  isdrngo2  38209  erimeq2  39014  prter3  39258  islshpsm  39356  lsatfixedN  39385  lrelat  39390  eqlkr2  39476  lshpkrlem1  39486  lfl1dim  39497  eqlkr4  39541  ishlat3N  39730  hlsupr2  39763  hlrelat5N  39777  hlrelat  39778  cvrval5  39791  cvrat42  39820  athgt  39832  3dim0  39833  islln3  39886  llnexatN  39897  islpln3  39909  islvol3  39952  islvol5  39955  isline4N  40153  polval2N  40282  4atex3  40457  cdleme0ex2N  40600  cdlemefrs29cpre1  40774  cdlemb3  40982  cdlemg33c  41084  cdlemg33e  41086  dia1dim2  41438  cdlemm10N  41494  dib1dim2  41544  diclspsn  41570  dih1dimatlem  41705  dihatexv2  41715  djhcvat42  41791  dihjat1lem  41804  dvh4dimat  41814  dvh2dimatN  41816  lcfrlem9  41926  mapdval4N  42008  mapdcv  42036  ef11d  42709  cxp112d  42711  cxp111d  42712  sn-sup3d  42862  fimgmcyc  42904  infdesc  43001  elrfirn  43052  elrfirn2  43053  mrefg3  43065  diophin  43129  diophun  43130  diophren  43170  rmxycomplete  43274  wepwsolem  43399  fnwe2lem2  43408  islssfg  43427  unielss  43575  onmaxnelsup  43580  onsupnmax  43585  onsupeqnmax  43604  tfsconcat0i  43702  ntrneineine0lem  44439  ntrneineine1lem  44440  ntrneiel2  44442  extoimad  44520  grumnudlem  44641  modelac8prim  45348  supsubc  45712  infxrbnd2  45727  supminfxr  45822  evthiccabs  45856  elicores  45893  clim2f  45994  clim2cf  46008  clim0cf  46012  clim2f2  46028  limsupub  46062  limsupmnflem  46078  limsupre2lem  46082  limsuplt2  46111  liminfreuzlem  46160  liminfltlem  46162  liminflimsupclim  46165  xlimmnfmpt  46201  xlimpnfmpt  46202  fourierdlem73  46537  fourierdlem83  46547  meaiuninc3v  46842  ovolval2  47002  cfsetsnfsetfo  47420  dfaimafn  47525  iccelpart  47793  sprsymrelf  47855  sprsymrelfo  47857  fmtnoprmfac1  47925  fmtnoprmfac2  47927  fmtnofac2lem  47928  dfeven2  48009  dfodd3  48010  dfvopnbgr2  48213  usgrgrtrirex  48310  stgredgiun  48318  uspgrsprfo  48508  elbigo2  48912  rrxlinesc  49095  rrxlinec  49096  rrx2line  49100  rrx2vlinest  49101  itsclquadeu  49137