Theorem rexbidva 3215

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∈ wcel 2110  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-rex 3067

This theorem is referenced by:  rexbidv  3216  2rexbiia  3217  2rexbidva  3218  rexeqbidva  3332  frinxp  5631  onfr  6252  dfimafn  6775  funimass4  6777  fliftel  7118  fliftf  7124  isomin  7146  f1oiso  7160  releldm2  7814  oaass  8289  qsinxp  8475  qliftel  8482  fimaxg  8918  ordunifi  8921  supisolem  9089  fiming  9114  wemapwe  9312  cflim2  9877  cfsmolem  9884  alephsing  9890  brdom7disj  10145  brdom6disj  10146  alephreg  10196  nqereu  10543  1idpr  10643  map2psrpr  10724  axsup  10908  rereccl  11550  sup3  11789  infm3  11791  supadd  11800  creur  11824  creui  11825  nndiv  11876  nnrecl  12088  rpnnen1lem2  12573  rpnnen1lem1  12574  rpnnen1lem3  12575  rpnnen1lem5  12577  supxrbnd1  12911  supxrbnd2  12912  supxrbnd  12918  rabssnn0fi  13559  mptnn0fsupp  13570  expnlbnd  13800  wrdl3s3  14529  limsuplt  15040  clim2  15065  clim2c  15066  clim0c  15068  ello12  15077  elo12  15088  rlimresb  15126  climabs0  15146  sumeq2ii  15257  mertens  15450  prodeq2ii  15475  zprod  15499  nndivides  15825  alzdvds  15881  oddm1even  15904  oddnn02np1  15909  oddge22np1  15910  evennn02n  15911  evennn2n  15912  divalglem4  15957  divalgb  15965  modremain  15969  modprmn0modprm0  16360  vdwlem6  16539  vdwlem11  16544  vdw  16547  ramval  16561  imasleval  17046  dfiso3  17278  fullestrcsetc  17658  fullsetcestrc  17673  isipodrs  18043  ipodrsfi  18045  gsumpropd2lem  18151  mndpropd  18198  grppropd  18382  conjnmzb  18657  symgextfo  18814  symgfixfo  18831  sylow1lem2  18988  sylow3lem1  19016  sylow3lem3  19018  lsmelvalm  19040  lsmass  19059  iscyg3  19270  ghmcyg  19281  cycsubgcyg  19286  pgpfac1lem2  19462  pgpfac1lem4  19465  ablfac2  19476  dvdsr02  19674  crngunit  19680  dvdsrpropd  19714  lpigen  20294  znunit  20528  elfilspd  20765  scmatmats  21408  symgmatr01  21551  isclo  21984  iscnp3  22141  lmbrf  22157  cncnp  22177  lmss  22195  isnrm2  22255  cmpfi  22305  1stcfb  22342  1stccnp  22359  ptrescn  22536  txkgen  22549  xkoinjcn  22584  trfil3  22785  fmid  22857  lmflf  22902  txflf  22903  ptcmplem3  22951  tsmsf1o  23042  ucnprima  23179  metrest  23422  metcnp  23439  metcnp2  23440  txmetcnp  23445  metuel2  23463  metustbl  23464  psmetutop  23465  metucn  23469  evth2  23857  lmmbrf  24159  iscfil2  24163  fmcfil  24169  iscau2  24174  iscau4  24176  iscauf  24177  caucfil  24180  iscmet3lem3  24187  cfilresi  24192  causs  24195  lmclim  24200  ivth2  24352  ovolfioo  24364  ovolficc  24365  ovolshftlem1  24406  ovolscalem1  24410  volsup2  24502  ismbf3d  24551  mbfaddlem  24557  mbfsup  24561  mbfinf  24562  itg2seq  24640  itg2gt0  24658  ellimc2  24774  ellimc3  24776  rolle  24887  cmvth  24888  mvth  24889  dvlip  24890  dvivth  24907  lhop1lem  24910  deg1ldg  24990  ulm2  25277  ulmdvlem3  25294  dcubic  25729  mcubic  25730  cubic2  25731  rlimcnp  25848  ftalem3  25957  isppw2  25997  lgsquadlem2  26262  2lgslem1a  26272  dchrmusumlema  26374  dchrisum0lema  26395  tglowdim2l  26741  mirreu3  26745  oppcom  26835  iscgra1  26901  axsegcon  27018  axpasch  27032  axcontlem7  27061  usgr2pth0  27852  usgr2wspthon  28049  elwwlks2  28050  elwspths2spth  28051  rusgrnumwwlks  28058  clwwlkfo  28133  eclclwwlkn1  28158  eucrctshift  28326  fusgreg2wsp  28419  nmobndi  28856  nmounbi  28857  nmoo0  28872  h2hcau  29060  h2hlm  29061  shsel3  29396  pjhtheu2  29497  chscllem2  29719  adjbdln  30164  branmfn  30186  pjimai  30257  chrelati  30445  cdj3lem3  30519  cdj3lem3b  30521  dfimafnf  30690  ofpreima  30722  isarchi2  31158  submarchi  31159  archirng  31161  archiabl  31171  isarchiofld  31235  ellspds  31278  lsmssass  31304  grplsm0l  31305  fedgmullem2  31425  zarcls  31538  ordtconnlem1  31588  lmdvg  31617  esumfsup  31750  dya2icoseg2  31957  eulerpartlemgh  32057  ballotlemodife  32176  ballotlemsima  32194  nummin  32776  erdszelem10  32875  iscvm  32934  eldifsucnn  33410  ttrcltr  33515  wsuclem  33556  cofcutr  33829  lrrecfr  33837  addsid1  33864  addscom  33866  seglelin  34155  outsideofeu  34170  opnrebl  34246  opnrebl2  34247  filnetlem4  34307  bj-finsumval0  35191  phpreu  35498  ptrest  35513  poimirlem3  35517  poimirlem4  35518  poimirlem17  35531  poimirlem26  35540  poimirlem27  35541  broucube  35548  mblfinlem1  35551  lmclim2  35653  caures  35655  isbnd3b  35680  heiborlem7  35712  heiborlem10  35715  rrncmslem  35727  isdrngo2  35853  erim2  36526  prter3  36633  islshpsm  36731  lsatfixedN  36760  lrelat  36765  eqlkr2  36851  lshpkrlem1  36861  lfl1dim  36872  eqlkr4  36916  ishlat3N  37105  hlsupr2  37138  hlrelat5N  37152  hlrelat  37153  cvrval5  37166  cvrat42  37195  athgt  37207  3dim0  37208  islln3  37261  llnexatN  37272  islpln3  37284  islvol3  37327  islvol5  37330  isline4N  37528  polval2N  37657  4atex3  37832  cdleme0ex2N  37975  cdlemefrs29cpre1  38149  cdlemb3  38357  cdlemg33c  38459  cdlemg33e  38461  dia1dim2  38813  cdlemm10N  38869  dib1dim2  38919  diclspsn  38945  dih1dimatlem  39080  dihatexv2  39090  djhcvat42  39166  dihjat1lem  39179  dvh4dimat  39189  dvh2dimatN  39191  lcfrlem9  39301  mapdval4N  39383  mapdcv  39411  infdesc  40183  elrfirn  40220  elrfirn2  40221  mrefg3  40233  diophin  40297  diophun  40298  diophren  40338  rmxycomplete  40442  wepwsolem  40570  fnwe2lem2  40579  islssfg  40598  ntrneineine0lem  41370  ntrneineine1lem  41371  ntrneiel2  41373  extoimad  41452  grumnudlem  41576  supsubc  42565  infxrbnd2  42581  supminfxr  42679  evthiccabs  42709  elicores  42746  clim2f  42852  clim2cf  42866  clim0cf  42870  clim2f2  42886  limsupub  42920  limsupmnflem  42936  limsupre2lem  42940  limsuplt2  42969  liminfreuzlem  43018  liminfltlem  43020  liminflimsupclim  43023  xlimmnfmpt  43059  xlimpnfmpt  43060  fourierdlem73  43395  fourierdlem83  43405  meaiuninc3v  43697  ovolval2  43857  cfsetsnfsetfo  44226  dfaimafn  44329  iccelpart  44558  sprsymrelf  44620  sprsymrelfo  44622  fmtnoprmfac1  44690  fmtnoprmfac2  44692  fmtnofac2lem  44693  dfeven2  44774  dfodd3  44775  isomuspgrlem2d  44956  uspgrsprfo  44983  elbigo2  45571  rrxlinesc  45754  rrxlinec  45755  rrx2line  45759  rrx2vlinest  45760  itsclquadeu  45796