Theorem rexbidva 3151

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 3149	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  3153  2rexbiia  3190  2rexbidva  3192  rexeqbidva  3296  frinxp  5702  onfr  6346  dfimafn  6885  funimass4  6887  fliftel  7246  fliftf  7252  isomin  7274  f1oiso  7288  releldm2  7978  oaass  8479  eldifsucnn  8582  cofonr  8592  naddunif  8611  qsinxp  8720  qliftel  8727  fimaxg  9176  ordunifi  9179  supisolem  9364  fiming  9390  wemapwe  9593  ttrcltr  9612  ttrclse  9623  frmin  9645  cflim2  10157  cfsmolem  10164  alephsing  10170  brdom7disj  10425  brdom6disj  10426  alephreg  10476  nqereu  10823  1idpr  10923  map2psrpr  11004  axsup  11191  rereccl  11842  sup3  12082  infm3  12084  supadd  12093  creur  12122  creui  12123  nndiv  12174  nnrecl  12382  rpnnen1lem2  12878  rpnnen1lem1  12879  rpnnen1lem3  12880  rpnnen1lem5  12882  supxrbnd1  13223  supxrbnd2  13224  supxrbnd  13230  rabssnn0fi  13893  mptnn0fsupp  13904  expnlbnd  14140  wrdl3s3  14869  limsuplt  15386  clim2  15411  clim2c  15412  clim0c  15414  ello12  15423  elo12  15434  rlimresb  15472  climabs0  15492  sumeq2ii  15600  mertens  15793  prodeq2ii  15818  zprod  15844  nndivides  16173  alzdvds  16231  oddm1even  16254  oddnn02np1  16259  oddge22np1  16260  evennn02n  16261  evennn2n  16262  divalglem4  16307  divalgb  16315  modremain  16319  modprmn0modprm0  16719  vdwlem6  16898  vdwlem11  16903  vdw  16906  ramval  16920  imasleval  17445  dfiso3  17680  fullestrcsetc  18057  fullsetcestrc  18072  isipodrs  18443  ipodrsfi  18445  gsumpropd2lem  18553  mndpropd  18633  grppropd  18830  qus0subgbas  19077  conjnmzb  19132  symgextfo  19301  symgfixfo  19318  sylow1lem2  19478  sylow3lem1  19506  sylow3lem3  19508  lsmelvalm  19530  lsmass  19548  iscyg3  19765  ghmcyg  19775  cycsubgcyg  19780  pgpfac1lem2  19956  pgpfac1lem4  19959  ablfac2  19970  dvdsr02  20257  crngunit  20263  dvdsrpropd  20301  rngqiprngimfo  21208  lpigen  21242  pzriprnglem10  21397  znunit  21470  elfilspd  21710  psdmul  22051  scmatmats  22396  symgmatr01  22539  isclo  22972  iscnp3  23129  lmbrf  23145  cncnp  23165  lmss  23183  isnrm2  23243  cmpfi  23293  1stcfb  23330  1stccnp  23347  ptrescn  23524  txkgen  23537  xkoinjcn  23572  trfil3  23773  fmid  23845  lmflf  23890  txflf  23891  ptcmplem3  23939  tsmsf1o  24030  ucnprima  24167  metrest  24410  metcnp  24427  metcnp2  24428  txmetcnp  24433  metuel2  24451  metustbl  24452  psmetutop  24453  metucn  24457  evth2  24857  lmmbrf  25160  iscfil2  25164  fmcfil  25170  iscau2  25175  iscau4  25177  iscauf  25178  caucfil  25181  iscmet3lem3  25188  cfilresi  25193  causs  25196  lmclim  25201  ivth2  25354  ovolfioo  25366  ovolficc  25367  ovolshftlem1  25408  ovolscalem1  25412  volsup2  25504  ismbf3d  25553  mbfaddlem  25559  mbfsup  25563  mbfinf  25564  itg2seq  25641  itg2gt0  25659  ellimc2  25776  ellimc3  25778  rolle  25892  cmvth  25893  cmvthOLD  25894  mvth  25895  dvlip  25896  dvivth  25913  lhop1lem  25916  deg1ldg  25995  ulm2  26292  ulmdvlem3  26309  dcubic  26754  mcubic  26755  cubic2  26756  rlimcnp  26873  ftalem3  26983  isppw2  27023  lgsquadlem2  27290  2lgslem1a  27300  dchrmusumlema  27402  dchrisum0lema  27423  cofcutr  27837  lrrecfr  27855  addsrid  27876  addscom  27878  addsuniflem  27913  addsass  27917  addsbday  27929  negsunif  27966  mulsrid  28021  mulsasslem3  28073  n0s0suc  28239  zs12ge0  28360  renegscl  28367  readdscl  28368  remulscllem2  28370  remulscl  28371  tglowdim2l  28595  mirreu3  28599  oppcom  28689  iscgra1  28755  axsegcon  28872  axpasch  28886  axcontlem7  28915  usgr2pth0  29710  usgr2wspthon  29910  elwwlks2  29911  elwspths2spth  29912  rusgrnumwwlks  29919  clwwlkfo  29994  eclclwwlkn1  30019  eucrctshift  30187  fusgreg2wsp  30280  nmobndi  30719  nmounbi  30720  nmoo0  30735  h2hcau  30923  h2hlm  30924  shsel3  31259  pjhtheu2  31360  chscllem2  31582  adjbdln  32027  branmfn  32049  pjimai  32120  chrelati  32308  cdj3lem3  32382  cdj3lem3b  32384  dfimafnf  32579  ofpreima  32608  isarchi2  33127  submarchi  33128  archirng  33130  archiabl  33140  isarchiofld  33141  ellspds  33305  dvdsruasso2  33323  lsmssass  33339  grplsm0l  33340  fedgmullem2  33597  elirng  33653  zarcls  33841  ordtconnlem1  33891  lmdvg  33920  esumfsup  34037  dya2icoseg2  34246  eulerpartlemgh  34346  ballotlemodife  34466  ballotlemsima  34484  nummin  35058  erdszelem10  35173  iscvm  35232  wsuclem  35799  seglelin  36090  outsideofeu  36105  opnrebl  36294  opnrebl2  36295  filnetlem4  36355  bj-finsumval0  37259  phpreu  37584  ptrest  37599  poimirlem3  37603  poimirlem4  37604  poimirlem17  37617  poimirlem26  37626  poimirlem27  37627  broucube  37634  mblfinlem1  37637  lmclim2  37738  caures  37740  isbnd3b  37765  heiborlem7  37797  heiborlem10  37800  rrncmslem  37812  isdrngo2  37938  erimeq2  38656  prter3  38861  islshpsm  38959  lsatfixedN  38988  lrelat  38993  eqlkr2  39079  lshpkrlem1  39089  lfl1dim  39100  eqlkr4  39144  ishlat3N  39333  hlsupr2  39366  hlrelat5N  39380  hlrelat  39381  cvrval5  39394  cvrat42  39423  athgt  39435  3dim0  39436  islln3  39489  llnexatN  39500  islpln3  39512  islvol3  39555  islvol5  39558  isline4N  39756  polval2N  39885  4atex3  40060  cdleme0ex2N  40203  cdlemefrs29cpre1  40377  cdlemb3  40585  cdlemg33c  40687  cdlemg33e  40689  dia1dim2  41041  cdlemm10N  41097  dib1dim2  41147  diclspsn  41173  dih1dimatlem  41308  dihatexv2  41318  djhcvat42  41394  dihjat1lem  41407  dvh4dimat  41417  dvh2dimatN  41419  lcfrlem9  41529  mapdval4N  41611  mapdcv  41639  ef11d  42312  cxp112d  42314  cxp111d  42315  sn-sup3d  42465  fimgmcyc  42507  infdesc  42616  elrfirn  42668  elrfirn2  42669  mrefg3  42681  diophin  42745  diophun  42746  diophren  42786  rmxycomplete  42890  wepwsolem  43015  fnwe2lem2  43024  islssfg  43043  unielss  43191  onmaxnelsup  43196  onsupnmax  43201  onsupeqnmax  43220  tfsconcat0i  43318  ntrneineine0lem  44056  ntrneineine1lem  44057  ntrneiel2  44059  extoimad  44137  grumnudlem  44258  modelac8prim  44966  supsubc  45333  infxrbnd2  45348  supminfxr  45443  evthiccabs  45477  elicores  45514  clim2f  45617  clim2cf  45631  clim0cf  45635  clim2f2  45651  limsupub  45685  limsupmnflem  45701  limsupre2lem  45705  limsuplt2  45734  liminfreuzlem  45783  liminfltlem  45785  liminflimsupclim  45788  xlimmnfmpt  45824  xlimpnfmpt  45825  fourierdlem73  46160  fourierdlem83  46170  meaiuninc3v  46465  ovolval2  46625  cfsetsnfsetfo  47044  dfaimafn  47149  iccelpart  47417  sprsymrelf  47479  sprsymrelfo  47481  fmtnoprmfac1  47549  fmtnoprmfac2  47551  fmtnofac2lem  47552  dfeven2  47633  dfodd3  47634  dfvopnbgr2  47837  usgrgrtrirex  47934  stgredgiun  47942  uspgrsprfo  48132  elbigo2  48537  rrxlinesc  48720  rrxlinec  48721  rrx2line  48725  rrx2vlinest  48726  itsclquadeu  48762