Theorem rexbidva 3187

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-rex 3090

This theorem is referenced by:  rexbidv  3189  2rexbiia  3226  2rexbidva  3228  rexeqbidva  3330  frinxp  5744  onfr  6400  dfimafn  6943  funimass4  6945  fliftel  7307  fliftf  7313  isomin  7335  f1oiso  7349  releldm2  8036  oaass  8542  eldifsucnn  8646  cofonr  8656  naddunif  8676  qsinxp  8787  qliftel  8794  fimaxg  9243  ordunifi  9246  supisolem  9430  fiming  9456  wemapwe  9662  ttrcltr  9681  ttrclse  9692  frmin  9717  cflim2  10242  cfsmolem  10249  alephsing  10255  brdom7disj  10510  brdom6disj  10511  alephreg  10562  nqereu  10909  1idpr  11009  map2psrpr  11090  axsup  11280  rereccl  11928  sup3  12167  infm3  12169  supadd  12178  creur  12207  creui  12208  nndiv  12277  nnrecl  12497  rpnnen1lem2  12996  rpnnen1lem1  12997  rpnnen1lem3  12998  rpnnen1lem5  13000  supxrbnd1  13342  supxrbnd2  13343  supxrbnd  13349  rabssnn0fi  14018  mptnn0fsupp  14029  expnlbnd  14265  wrdl3s3  14995  limsuplt  15526  clim2  15551  clim2c  15552  clim0c  15554  ello12  15563  elo12  15574  rlimresb  15612  climabs0  15632  sumeq2ii  15740  mertens  15936  prodeq2ii  15961  zprod  15987  nndivides  16315  alzdvds  16373  oddm1even  16396  oddnn02np1  16401  oddge22np1  16402  evennn02n  16403  evennn2n  16404  divalglem4  16449  divalgb  16457  modremain  16461  modprmn0modprm0  16862  vdwlem6  17041  vdwlem11  17046  vdw  17049  ramval  17063  imasleval  17590  dfiso3  17825  fullestrcsetc  18202  fullsetcestrc  18217  isipodrs  18588  ipodrsfi  18590  gsumpropd2lem  18732  mndpropd  18812  grppropd  19013  qus0subgbas  19264  conjnmzb  19318  symgextfo  19487  symgfixfo  19504  sylow1lem2  19664  sylow3lem1  19692  sylow3lem3  19694  lsmelvalm  19716  lsmass  19734  iscyg3  19951  ghmcyg  19961  cycsubgcyg  19966  pgpfac1lem2  20142  pgpfac1lem4  20145  ablfac2  20156  dvdsr02  20450  crngunit  20456  dvdsrpropd  20494  rngqiprngimfo  21441  lpigen  21503  pzriprnglem10  21640  znunit  21713  elfilspd  21953  psdmul  22329  scmatmats  22668  symgmatr01  22811  isclo  23244  iscnp3  23401  lmbrf  23417  cncnp  23437  lmss  23455  isnrm2  23515  cmpfi  23565  1stcfb  23602  1stccnp  23619  ptrescn  23796  txkgen  23809  xkoinjcn  23844  trfil3  24045  fmid  24117  lmflf  24162  txflf  24163  ptcmplem3  24211  tsmsf1o  24302  ucnprima  24438  metrest  24681  metcnp  24698  metcnp2  24699  txmetcnp  24704  metuel2  24722  metustbl  24723  psmetutop  24724  metucn  24728  evth2  25119  lmmbrf  25421  iscfil2  25425  fmcfil  25431  iscau2  25436  iscau4  25438  iscauf  25439  caucfil  25442  iscmet3lem3  25449  cfilresi  25454  causs  25457  lmclim  25462  ivth2  25614  ovolfioo  25626  ovolficc  25627  ovolshftlem1  25668  ovolscalem1  25672  volsup2  25764  ismbf3d  25813  mbfaddlem  25819  mbfsup  25823  mbfinf  25824  itg2seq  25901  itg2gt0  25919  ellimc2  26036  ellimc3  26038  rolle  26149  cmvth  26150  mvth  26151  dvlip  26152  dvivth  26169  lhop1lem  26172  deg1ldg  26249  ulm2  26548  ulmdvlem3  26565  dcubic  27011  mcubic  27012  cubic2  27013  rlimcnp  27130  ftalem3  27239  isppw2  27279  lgsquadlem2  27545  2lgslem1a  27555  dchrmusumlema  27657  dchrisum0lema  27678  cofcutr  28117  lrrecfr  28136  addsrid  28157  addscom  28159  addsuniflem  28194  addsass  28198  addbday  28211  negsunif  28248  mulsrid  28306  mulsasslem3  28358  n0s0suc  28535  z12sge0  28676  elreno2  28688  renegscl  28691  readdscl  28692  remulscllem2  28694  remulscl  28695  tglowdim2l  28924  mirreu3  28931  oppcom  29025  iscgra1  29121  axsegcon  29277  axpasch  29291  axcontlem7  29320  usgr2pth0  30114  usgr2wspthon  30317  elwwlks2  30318  elwspths2spth  30319  rusgrnumwwlks  30326  clwwlkfo  30401  eclclwwlkn1  30426  eucrctshift  30594  fusgreg2wsp  30687  nmobndi  31127  nmounbi  31128  nmoo0  31143  h2hcau  31331  h2hlm  31332  shsel3  31667  pjhtheu2  31768  chscllem2  31990  adjbdln  32435  branmfn  32457  pjimai  32528  chrelati  32716  cdj3lem3  32790  cdj3lem3b  32792  dfimafnf  32981  ofpreima  33010  isarchi2  33505  submarchi  33506  archirng  33508  archiabl  33518  isarchiofld  33519  isunitc  33561  ellspds  33683  dvdsruasso2  33699  lsmssass  33711  grplsm0l  33712  fedgmullem2  34020  elirng  34076  zarcls  34264  ordtconnlem1  34314  lmdvg  34343  esumfsup  34460  dya2icoseg2  34668  eulerpartlemgh  34768  ballotlemodife  34888  ballotlemsima  34906  nummin  35484  erdszelem10  35692  iscvm  35751  wsuclem  36315  seglelin  36608  outsideofeu  36623  ltnadd  36695  naddle  36696  opnrebl  36831  opnrebl2  36832  filnetlem4  36892  bj-finsumval0  37929  phpreu  38255  ptrest  38270  poimirlem3  38274  poimirlem4  38275  poimirlem17  38288  poimirlem26  38297  poimirlem27  38298  broucube  38305  mblfinlem1  38308  lmclim2  38409  caures  38411  isbnd3b  38436  heiborlem7  38468  heiborlem10  38471  rrncmslem  38483  isdrngo2  38609  erimeq2  39412  prter3  39656  islshpsm  39754  lsatfixedN  39783  lrelat  39788  eqlkr2  39874  lshpkrlem1  39884  lfl1dim  39895  eqlkr4  39939  ishlat3N  40128  hlsupr2  40161  hlrelat5N  40175  hlrelat  40176  cvrval5  40189  cvrat42  40218  athgt  40230  3dim0  40231  islln3  40284  llnexatN  40295  islpln3  40307  islvol3  40350  islvol5  40353  isline4N  40551  polval2N  40680  4atex3  40855  cdleme0ex2N  40998  cdlemefrs29cpre1  41172  cdlemb3  41380  cdlemg33c  41482  cdlemg33e  41484  dia1dim2  41836  cdlemm10N  41892  dib1dim2  41942  diclspsn  41968  dih1dimatlem  42103  dihatexv2  42113  djhcvat42  42189  dihjat1lem  42202  dvh4dimat  42212  dvh2dimatN  42214  lcfrlem9  42324  mapdval4N  42406  mapdcv  42434  ef11d  43100  cxp112d  43102  cxp111d  43103  sn-sup3d  43266  fimgmcyc  43302  infdesc  43375  elrfirn  43426  elrfirn2  43427  mrefg3  43439  diophin  43503  diophun  43504  diophren  43540  rmxycomplete  43644  wepwsolem  43769  fnwe2lem2  43778  islssfg  43797  unielss  43945  onmaxnelsup  43950  onsupnmax  43955  onsupeqnmax  43974  tfsconcat0i  44072  ntrneineine0lem  44809  ntrneineine1lem  44810  ntrneiel2  44812  extoimad  44890  grumnudlem  44995  modelac8prim  45701  supsubc  46069  infxrbnd2  46084  supminfxr  46178  evthiccabs  46212  elicores  46249  clim2f  46350  clim2cf  46364  clim0cf  46368  clim2f2  46384  limsupub  46418  limsupmnflem  46434  limsupre2lem  46438  limsuplt2  46467  liminfreuzlem  46516  liminfltlem  46518  liminflimsupclim  46521  xlimmnfmpt  46557  xlimpnfmpt  46558  fourierdlem73  46893  fourierdlem83  46903  meaiuninc3v  47198  ovolval2  47358  cfsetsnfsetfo  47797  dfaimafn  47902  iccelpart  48182  sprsymrelf  48244  sprsymrelfo  48246  nprmmul1  48276  nprmmul3  48278  fmtnoprmfac1  48317  fmtnoprmfac2  48319  fmtnofac2lem  48320  dfeven2  48414  dfodd3  48415  dfvopnbgr2  48618  usgrgrtrirex  48715  stgredgiun  48723  uspgrsprfo  48913  elbigo2  49332  rrxlinesc  49515  rrxlinec  49516  rrx2line  49520  rrx2vlinest  49521  itsclquadeu  49557