Theorem rexbidva 3155

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  rexbidv  3157  2rexbiia  3198  2rexbidva  3200  rexeqbidva  3306  frinxp  5721  onfr  6371  dfimafn  6923  funimass4  6925  fliftel  7284  fliftf  7290  isomin  7312  f1oiso  7326  releldm2  8022  oaass  8525  eldifsucnn  8628  cofonr  8638  naddunif  8657  qsinxp  8766  qliftel  8773  fimaxg  9234  ordunifi  9237  supisolem  9425  fiming  9451  wemapwe  9650  ttrcltr  9669  ttrclse  9680  frmin  9702  cflim2  10216  cfsmolem  10223  alephsing  10229  brdom7disj  10484  brdom6disj  10485  alephreg  10535  nqereu  10882  1idpr  10982  map2psrpr  11063  axsup  11249  rereccl  11900  sup3  12140  infm3  12142  supadd  12151  creur  12180  creui  12181  nndiv  12232  nnrecl  12440  rpnnen1lem2  12936  rpnnen1lem1  12937  rpnnen1lem3  12938  rpnnen1lem5  12940  supxrbnd1  13281  supxrbnd2  13282  supxrbnd  13288  rabssnn0fi  13951  mptnn0fsupp  13962  expnlbnd  14198  wrdl3s3  14928  limsuplt  15445  clim2  15470  clim2c  15471  clim0c  15473  ello12  15482  elo12  15493  rlimresb  15531  climabs0  15551  sumeq2ii  15659  mertens  15852  prodeq2ii  15877  zprod  15903  nndivides  16232  alzdvds  16290  oddm1even  16313  oddnn02np1  16318  oddge22np1  16319  evennn02n  16320  evennn2n  16321  divalglem4  16366  divalgb  16374  modremain  16378  modprmn0modprm0  16778  vdwlem6  16957  vdwlem11  16962  vdw  16965  ramval  16979  imasleval  17504  dfiso3  17735  fullestrcsetc  18112  fullsetcestrc  18127  isipodrs  18496  ipodrsfi  18498  gsumpropd2lem  18606  mndpropd  18686  grppropd  18883  qus0subgbas  19130  conjnmzb  19185  symgextfo  19352  symgfixfo  19369  sylow1lem2  19529  sylow3lem1  19557  sylow3lem3  19559  lsmelvalm  19581  lsmass  19599  iscyg3  19816  ghmcyg  19826  cycsubgcyg  19831  pgpfac1lem2  20007  pgpfac1lem4  20010  ablfac2  20021  dvdsr02  20281  crngunit  20287  dvdsrpropd  20325  rngqiprngimfo  21211  lpigen  21245  pzriprnglem10  21400  znunit  21473  elfilspd  21712  psdmul  22053  scmatmats  22398  symgmatr01  22541  isclo  22974  iscnp3  23131  lmbrf  23147  cncnp  23167  lmss  23185  isnrm2  23245  cmpfi  23295  1stcfb  23332  1stccnp  23349  ptrescn  23526  txkgen  23539  xkoinjcn  23574  trfil3  23775  fmid  23847  lmflf  23892  txflf  23893  ptcmplem3  23941  tsmsf1o  24032  ucnprima  24169  metrest  24412  metcnp  24429  metcnp2  24430  txmetcnp  24435  metuel2  24453  metustbl  24454  psmetutop  24455  metucn  24459  evth2  24859  lmmbrf  25162  iscfil2  25166  fmcfil  25172  iscau2  25177  iscau4  25179  iscauf  25180  caucfil  25183  iscmet3lem3  25190  cfilresi  25195  causs  25198  lmclim  25203  ivth2  25356  ovolfioo  25368  ovolficc  25369  ovolshftlem1  25410  ovolscalem1  25414  volsup2  25506  ismbf3d  25555  mbfaddlem  25561  mbfsup  25565  mbfinf  25566  itg2seq  25643  itg2gt0  25661  ellimc2  25778  ellimc3  25780  rolle  25894  cmvth  25895  cmvthOLD  25896  mvth  25897  dvlip  25898  dvivth  25915  lhop1lem  25918  deg1ldg  25997  ulm2  26294  ulmdvlem3  26311  dcubic  26756  mcubic  26757  cubic2  26758  rlimcnp  26875  ftalem3  26985  isppw2  27025  lgsquadlem2  27292  2lgslem1a  27302  dchrmusumlema  27404  dchrisum0lema  27425  cofcutr  27832  lrrecfr  27850  addsrid  27871  addscom  27873  addsuniflem  27908  addsass  27912  addsbday  27924  negsunif  27961  mulsrid  28016  mulsasslem3  28068  n0s0suc  28234  zs12ge0  28342  renegscl  28349  readdscl  28350  remulscllem2  28352  remulscl  28353  tglowdim2l  28577  mirreu3  28581  oppcom  28671  iscgra1  28737  axsegcon  28854  axpasch  28868  axcontlem7  28897  usgr2pth0  29695  usgr2wspthon  29895  elwwlks2  29896  elwspths2spth  29897  rusgrnumwwlks  29904  clwwlkfo  29979  eclclwwlkn1  30004  eucrctshift  30172  fusgreg2wsp  30265  nmobndi  30704  nmounbi  30705  nmoo0  30720  h2hcau  30908  h2hlm  30909  shsel3  31244  pjhtheu2  31345  chscllem2  31567  adjbdln  32012  branmfn  32034  pjimai  32105  chrelati  32293  cdj3lem3  32367  cdj3lem3b  32369  dfimafnf  32560  ofpreima  32589  isarchi2  33139  submarchi  33140  archirng  33142  archiabl  33152  isarchiofld  33295  ellspds  33339  dvdsruasso2  33357  lsmssass  33373  grplsm0l  33374  fedgmullem2  33626  elirng  33681  zarcls  33864  ordtconnlem1  33914  lmdvg  33943  esumfsup  34060  dya2icoseg2  34269  eulerpartlemgh  34369  ballotlemodife  34489  ballotlemsima  34507  nummin  35081  erdszelem10  35187  iscvm  35246  wsuclem  35813  seglelin  36104  outsideofeu  36119  opnrebl  36308  opnrebl2  36309  filnetlem4  36369  bj-finsumval0  37273  phpreu  37598  ptrest  37613  poimirlem3  37617  poimirlem4  37618  poimirlem17  37631  poimirlem26  37640  poimirlem27  37641  broucube  37648  mblfinlem1  37651  lmclim2  37752  caures  37754  isbnd3b  37779  heiborlem7  37811  heiborlem10  37814  rrncmslem  37826  isdrngo2  37952  erimeq2  38670  prter3  38875  islshpsm  38973  lsatfixedN  39002  lrelat  39007  eqlkr2  39093  lshpkrlem1  39103  lfl1dim  39114  eqlkr4  39158  ishlat3N  39347  hlsupr2  39381  hlrelat5N  39395  hlrelat  39396  cvrval5  39409  cvrat42  39438  athgt  39450  3dim0  39451  islln3  39504  llnexatN  39515  islpln3  39527  islvol3  39570  islvol5  39573  isline4N  39771  polval2N  39900  4atex3  40075  cdleme0ex2N  40218  cdlemefrs29cpre1  40392  cdlemb3  40600  cdlemg33c  40702  cdlemg33e  40704  dia1dim2  41056  cdlemm10N  41112  dib1dim2  41162  diclspsn  41188  dih1dimatlem  41323  dihatexv2  41333  djhcvat42  41409  dihjat1lem  41422  dvh4dimat  41432  dvh2dimatN  41434  lcfrlem9  41544  mapdval4N  41626  mapdcv  41654  ef11d  42327  cxp112d  42329  cxp111d  42330  sn-sup3d  42480  fimgmcyc  42522  infdesc  42631  elrfirn  42683  elrfirn2  42684  mrefg3  42696  diophin  42760  diophun  42761  diophren  42801  rmxycomplete  42906  wepwsolem  43031  fnwe2lem2  43040  islssfg  43059  unielss  43207  onmaxnelsup  43212  onsupnmax  43217  onsupeqnmax  43236  tfsconcat0i  43334  ntrneineine0lem  44072  ntrneineine1lem  44073  ntrneiel2  44075  extoimad  44153  grumnudlem  44274  modelac8prim  44982  supsubc  45349  infxrbnd2  45365  supminfxr  45460  evthiccabs  45494  elicores  45531  clim2f  45634  clim2cf  45648  clim0cf  45652  clim2f2  45668  limsupub  45702  limsupmnflem  45718  limsupre2lem  45722  limsuplt2  45751  liminfreuzlem  45800  liminfltlem  45802  liminflimsupclim  45805  xlimmnfmpt  45841  xlimpnfmpt  45842  fourierdlem73  46177  fourierdlem83  46187  meaiuninc3v  46482  ovolval2  46642  cfsetsnfsetfo  47061  dfaimafn  47166  iccelpart  47434  sprsymrelf  47496  sprsymrelfo  47498  fmtnoprmfac1  47566  fmtnoprmfac2  47568  fmtnofac2lem  47569  dfeven2  47650  dfodd3  47651  dfvopnbgr2  47853  usgrgrtrirex  47949  stgredgiun  47957  uspgrsprfo  48136  elbigo2  48541  rrxlinesc  48724  rrxlinec  48725  rrx2line  48729  rrx2vlinest  48730  itsclquadeu  48766