Theorem rexbidva 3226

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

Assertion

Ref	Expression
rexbidva	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rexbidva

Step	Hyp	Ref	Expression
1		rexbidva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
2	1	pm5.32da 579	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
3	2	rexbidv2 3225	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∈ wcel 2107  ∃wrex 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-rex 3071

This theorem is referenced by:  rexbidv  3227  2rexbiia  3228  2rexbidva  3229  rexeqbidva  3356  frinxp  5670  onfr  6309  dfimafn  6841  funimass4  6843  fliftel  7189  fliftf  7195  isomin  7217  f1oiso  7231  releldm2  7893  oaass  8401  eldifsucnn  8503  qsinxp  8591  qliftel  8598  fimaxg  9070  ordunifi  9073  supisolem  9241  fiming  9266  wemapwe  9464  ttrcltr  9483  ttrclse  9494  frmin  9516  cflim2  10028  cfsmolem  10035  alephsing  10041  brdom7disj  10296  brdom6disj  10297  alephreg  10347  nqereu  10694  1idpr  10794  map2psrpr  10875  axsup  11059  rereccl  11702  sup3  11941  infm3  11943  supadd  11952  creur  11976  creui  11977  nndiv  12028  nnrecl  12240  rpnnen1lem2  12726  rpnnen1lem1  12727  rpnnen1lem3  12728  rpnnen1lem5  12730  supxrbnd1  13064  supxrbnd2  13065  supxrbnd  13071  rabssnn0fi  13715  mptnn0fsupp  13726  expnlbnd  13957  wrdl3s3  14686  limsuplt  15197  clim2  15222  clim2c  15223  clim0c  15225  ello12  15234  elo12  15245  rlimresb  15283  climabs0  15303  sumeq2ii  15414  mertens  15607  prodeq2ii  15632  zprod  15656  nndivides  15982  alzdvds  16038  oddm1even  16061  oddnn02np1  16066  oddge22np1  16067  evennn02n  16068  evennn2n  16069  divalglem4  16114  divalgb  16122  modremain  16126  modprmn0modprm0  16517  vdwlem6  16696  vdwlem11  16701  vdw  16704  ramval  16718  imasleval  17261  dfiso3  17494  fullestrcsetc  17877  fullsetcestrc  17892  isipodrs  18264  ipodrsfi  18266  gsumpropd2lem  18372  mndpropd  18419  grppropd  18603  conjnmzb  18878  symgextfo  19039  symgfixfo  19056  sylow1lem2  19213  sylow3lem1  19241  sylow3lem3  19243  lsmelvalm  19265  lsmass  19284  iscyg3  19495  ghmcyg  19506  cycsubgcyg  19511  pgpfac1lem2  19687  pgpfac1lem4  19690  ablfac2  19701  dvdsr02  19907  crngunit  19913  dvdsrpropd  19947  lpigen  20536  znunit  20780  elfilspd  21019  scmatmats  21669  symgmatr01  21812  isclo  22247  iscnp3  22404  lmbrf  22420  cncnp  22440  lmss  22458  isnrm2  22518  cmpfi  22568  1stcfb  22605  1stccnp  22622  ptrescn  22799  txkgen  22812  xkoinjcn  22847  trfil3  23048  fmid  23120  lmflf  23165  txflf  23166  ptcmplem3  23214  tsmsf1o  23305  ucnprima  23443  metrest  23689  metcnp  23706  metcnp2  23707  txmetcnp  23712  metuel2  23730  metustbl  23731  psmetutop  23732  metucn  23736  evth2  24132  lmmbrf  24435  iscfil2  24439  fmcfil  24445  iscau2  24450  iscau4  24452  iscauf  24453  caucfil  24456  iscmet3lem3  24463  cfilresi  24468  causs  24471  lmclim  24476  ivth2  24628  ovolfioo  24640  ovolficc  24641  ovolshftlem1  24682  ovolscalem1  24686  volsup2  24778  ismbf3d  24827  mbfaddlem  24833  mbfsup  24837  mbfinf  24838  itg2seq  24916  itg2gt0  24934  ellimc2  25050  ellimc3  25052  rolle  25163  cmvth  25164  mvth  25165  dvlip  25166  dvivth  25183  lhop1lem  25186  deg1ldg  25266  ulm2  25553  ulmdvlem3  25570  dcubic  26005  mcubic  26006  cubic2  26007  rlimcnp  26124  ftalem3  26233  isppw2  26273  lgsquadlem2  26538  2lgslem1a  26548  dchrmusumlema  26650  dchrisum0lema  26671  tglowdim2l  27020  mirreu3  27024  oppcom  27114  iscgra1  27180  axsegcon  27304  axpasch  27318  axcontlem7  27347  usgr2pth0  28142  usgr2wspthon  28339  elwwlks2  28340  elwspths2spth  28341  rusgrnumwwlks  28348  clwwlkfo  28423  eclclwwlkn1  28448  eucrctshift  28616  fusgreg2wsp  28709  nmobndi  29146  nmounbi  29147  nmoo0  29162  h2hcau  29350  h2hlm  29351  shsel3  29686  pjhtheu2  29787  chscllem2  30009  adjbdln  30454  branmfn  30476  pjimai  30547  chrelati  30735  cdj3lem3  30809  cdj3lem3b  30811  dfimafnf  30980  ofpreima  31011  isarchi2  31448  submarchi  31449  archirng  31451  archiabl  31461  isarchiofld  31525  ellspds  31573  lsmssass  31599  grplsm0l  31600  fedgmullem2  31720  zarcls  31833  ordtconnlem1  31883  lmdvg  31912  esumfsup  32047  dya2icoseg2  32254  eulerpartlemgh  32354  ballotlemodife  32473  ballotlemsima  32491  nummin  33072  erdszelem10  33171  iscvm  33230  wsuclem  33828  cofcutr  34101  lrrecfr  34109  addsid1  34136  addscom  34138  seglelin  34427  outsideofeu  34442  opnrebl  34518  opnrebl2  34519  filnetlem4  34579  bj-finsumval0  35465  phpreu  35770  ptrest  35785  poimirlem3  35789  poimirlem4  35790  poimirlem17  35803  poimirlem26  35812  poimirlem27  35813  broucube  35820  mblfinlem1  35823  lmclim2  35925  caures  35927  isbnd3b  35952  heiborlem7  35984  heiborlem10  35987  rrncmslem  35999  isdrngo2  36125  erim2  36796  prter3  36903  islshpsm  37001  lsatfixedN  37030  lrelat  37035  eqlkr2  37121  lshpkrlem1  37131  lfl1dim  37142  eqlkr4  37186  ishlat3N  37375  hlsupr2  37408  hlrelat5N  37422  hlrelat  37423  cvrval5  37436  cvrat42  37465  athgt  37477  3dim0  37478  islln3  37531  llnexatN  37542  islpln3  37554  islvol3  37597  islvol5  37600  isline4N  37798  polval2N  37927  4atex3  38102  cdleme0ex2N  38245  cdlemefrs29cpre1  38419  cdlemb3  38627  cdlemg33c  38729  cdlemg33e  38731  dia1dim2  39083  cdlemm10N  39139  dib1dim2  39189  diclspsn  39215  dih1dimatlem  39350  dihatexv2  39360  djhcvat42  39436  dihjat1lem  39449  dvh4dimat  39459  dvh2dimatN  39461  lcfrlem9  39571  mapdval4N  39653  mapdcv  39681  infdesc  40487  elrfirn  40524  elrfirn2  40525  mrefg3  40537  diophin  40601  diophun  40602  diophren  40642  rmxycomplete  40746  wepwsolem  40874  fnwe2lem2  40883  islssfg  40902  ntrneineine0lem  41700  ntrneineine1lem  41701  ntrneiel2  41703  extoimad  41782  grumnudlem  41910  supsubc  42899  infxrbnd2  42915  supminfxr  43011  evthiccabs  43041  elicores  43078  clim2f  43184  clim2cf  43198  clim0cf  43202  clim2f2  43218  limsupub  43252  limsupmnflem  43268  limsupre2lem  43272  limsuplt2  43301  liminfreuzlem  43350  liminfltlem  43352  liminflimsupclim  43355  xlimmnfmpt  43391  xlimpnfmpt  43392  fourierdlem73  43727  fourierdlem83  43737  meaiuninc3v  44029  ovolval2  44189  cfsetsnfsetfo  44565  dfaimafn  44668  iccelpart  44896  sprsymrelf  44958  sprsymrelfo  44960  fmtnoprmfac1  45028  fmtnoprmfac2  45030  fmtnofac2lem  45031  dfeven2  45112  dfodd3  45113  isomuspgrlem2d  45294  uspgrsprfo  45321  elbigo2  45909  rrxlinesc  46092  rrxlinec  46093  rrx2line  46097  rrx2vlinest  46098  itsclquadeu  46134