Theorem rexbidva 3189

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2146  ∃wrex 3091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3092

This theorem is used by:  rexbidv  3191  2rexbiia  3228  2rexbidva  3230  rexeqbidva  3332  frinxp  5746  onfr  6404  dfimafn  6947  funimass4  6949  fliftel  7316  fliftf  7322  isomin  7344  f1oiso  7358  releldm2  8046  oaass  8552  eldifsucnn  8656  cofonr  8666  naddunif  8686  qsinxp  8797  qliftel  8804  fimaxg  9254  ordunifi  9257  supisolem  9441  fiming  9467  wemapwe  9673  ttrcltr  9692  ttrclse  9703  frmin  9728  cflim2  10262  cfsmolem  10269  alephsing  10275  brdom7disj  10530  brdom6disj  10531  alephreg  10582  nqereu  10929  1idpr  11029  map2psrpr  11110  axsup  11300  rereccl  11948  sup3  12187  infm3  12189  supadd  12198  creur  12227  creui  12228  nndiv  12297  nnrecl  12517  rpnnen1lem2  13017  rpnnen1lem1  13018  rpnnen1lem3  13019  rpnnen1lem5  13021  supxrbnd1  13363  supxrbnd2  13364  supxrbnd  13370  rabssnn0fi  14040  mptnn0fsupp  14051  expnlbnd  14287  wrdl3s3  15023  limsuplt  15554  clim2  15579  clim2c  15580  clim0c  15582  ello12  15591  elo12  15602  rlimresb  15640  climabs0  15660  sumeq2ii  15768  mertens  15963  prodeq2ii  15988  zprod  16014  nndivides  16342  alzdvds  16400  oddm1even  16423  oddnn02np1  16428  oddge22np1  16429  evennn02n  16430  evennn2n  16431  divalglem4  16476  divalgb  16484  modremain  16488  modprmn0modprm0  16889  vdwlem6  17068  vdwlem11  17073  vdw  17076  ramval  17090  imasleval  17617  dfiso3  17852  fullestrcsetc  18229  fullsetcestrc  18244  isipodrs  18615  ipodrsfi  18617  mgmidpfod  18760  gsumpropd2lem  18769  mndpropd  18852  grppropd  19062  qus0subgbas  19313  conjnmzb  19367  symgextfo  19536  symgfixfo  19553  sylow1lem2  19713  sylow3lem1  19741  sylow3lem3  19743  lsmelvalm  19765  lsmass  19783  iscyg3  20000  ghmcyg  20010  cycsubgcyg  20015  pgpfac1lem2  20191  pgpfac1lem4  20194  ablfac2  20205  dvdsr02  20500  crngunit  20506  dvdsrpropd  20544  rngqiprngimfo  21491  lpigen  21553  pzriprnglem10  21690  znunit  21763  elfilspd  22003  psdmul  22379  scmatmats  22718  symgmatr01  22861  isclo  23294  iscnp3  23451  lmbrf  23467  cncnp  23487  lmss  23505  isnrm2  23565  cmpfi  23615  1stcfb  23652  1stccnp  23670  ptrescn  23847  txkgen  23860  xkoinjcn  23895  trfil3  24096  fmid  24168  lmflf  24213  txflf  24214  ptcmplem3  24262  tsmsf1o  24353  ucnprima  24489  metrest  24732  metcnp  24749  metcnp2  24750  txmetcnp  24755  metuel2  24773  metustbl  24774  psmetutop  24775  metucn  24779  evth2  25170  lmmbrf  25472  iscfil2  25476  fmcfil  25482  iscau2  25487  iscau4  25489  iscauf  25490  caucfil  25493  iscmet3lem3  25500  cfilresi  25505  causs  25508  lmclim  25513  ivth2  25665  ovolfioo  25677  ovolficc  25678  ovolshftlem1  25719  ovolscalem1  25723  volsup2  25815  ismbf3d  25864  mbfaddlem  25870  mbfsup  25874  mbfinf  25875  itg2seq  25952  itg2gt0  25970  ellimc2  26087  ellimc3  26089  rolle  26200  cmvth  26201  mvth  26202  dvlip  26203  dvivth  26220  lhop1lem  26223  deg1ldg  26300  ulm2  26599  ulmdvlem3  26616  dcubic  27062  mcubic  27063  cubic2  27064  rlimcnp  27181  ftalem3  27290  isppw2  27330  lgsquadlem2  27596  2lgslem1a  27606  dchrmusumlema  27708  dchrisum0lema  27729  cofcutr  28168  lrrecfr  28187  addsrid  28208  addscom  28210  addsuniflem  28245  addsass  28249  addbday  28262  negsunif  28299  mulsrid  28357  mulsasslem3  28409  n0s0suc  28586  z12sge0  28727  elreno2  28739  renegscl  28742  readdscl  28743  remulscllem2  28745  remulscl  28746  tglowdim2l  28975  mirreu3  28982  oppcom  29076  iscgra1  29172  axsegcon  29332  axpasch  29346  axcontlem7  29375  usgr2pth0  30178  usgr2wspthon  30384  elwwlks2  30385  elwspths2spth  30386  rusgrnumwwlks  30393  clwwlkfo  30468  eclclwwlkn1  30493  eucrctshift  30665  fusgreg2wsp  30758  nmobndi  31198  nmounbi  31199  nmoo0  31214  h2hcau  31402  h2hlm  31403  shsel3  31738  pjhtheu2  31839  chscllem2  32061  adjbdln  32506  branmfn  32528  pjimai  32599  chrelati  32787  cdj3lem3  32861  cdj3lem3b  32863  dfimafnf  33052  ofpreima  33081  isarchi2  33569  submarchi  33570  archirng  33572  archiabl  33582  isarchiofld  33583  isunitc  33625  ellspds  33747  dvdsruasso2  33763  lsmssass  33775  grplsm0l  33776  fedgmullem2  34084  elirng  34140  zarcls  34328  ordtconnlem1  34378  lmdvg  34407  esumfsup  34524  dya2icoseg2  34733  eulerpartlemgh  34833  ballotlemodife  34953  ballotlemsima  34971  nummin  35542  erdszelem10  35729  iscvm  35788  wsuclem  36352  seglelin  36645  outsideofeu  36660  ltnadd  36747  naddle  36748  opnrebl  36888  opnrebl2  36889  filnetlem4  36949  bj-finsumval0  37986  phpreu  38312  ptrest  38327  poimirlem3  38331  poimirlem4  38332  poimirlem17  38345  poimirlem26  38354  poimirlem27  38355  broucube  38362  mblfinlem1  38365  lmclim2  38467  caures  38469  isbnd3b  38494  heiborlem7  38526  heiborlem10  38529  rrncmslem  38541  isdrngo2  38667  erimeq2  39470  prter3  39714  islshpsm  39812  lsatfixedN  39841  lrelat  39846  eqlkr2  39932  lshpkrlem1  39942  lfl1dim  39953  eqlkr4  39997  ishlat3N  40186  hlsupr2  40219  hlrelat5N  40233  hlrelat  40234  cvrval5  40247  cvrat42  40276  athgt  40288  3dim0  40289  islln3  40342  llnexatN  40353  islpln3  40365  islvol3  40408  islvol5  40411  isline4N  40609  polval2N  40738  4atex3  40913  cdleme0ex2N  41056  cdlemefrs29cpre1  41230  cdlemb3  41438  cdlemg33c  41540  cdlemg33e  41542  dia1dim2  41894  cdlemm10N  41950  dib1dim2  42000  diclspsn  42026  dih1dimatlem  42161  dihatexv2  42171  djhcvat42  42247  dihjat1lem  42260  dvh4dimat  42270  dvh2dimatN  42272  lcfrlem9  42382  mapdval4N  42464  mapdcv  42492  ef11d  43158  cxp112d  43160  cxp111d  43161  sn-sup3d  43324  fimgmcyc  43360  infdesc  43433  elrfirn  43484  elrfirn2  43485  mrefg3  43497  diophin  43561  diophun  43562  diophren  43598  rmxycomplete  43702  wepwsolem  43827  fnwe2lem2  43836  islssfg  43855  unielss  44003  onmaxnelsup  44008  onsupnmax  44013  onsupeqnmax  44032  tfsconcat0i  44130  ntrneineine0lem  44867  ntrneineine1lem  44868  ntrneiel2  44870  extoimad  44948  grumnudlem  45053  modelac8prim  45759  supsubc  46127  infxrbnd2  46142  supminfxr  46236  evthiccabs  46270  elicores  46307  clim2f  46408  clim2cf  46422  clim0cf  46426  clim2f2  46442  limsupub  46476  limsupmnflem  46492  limsupre2lem  46496  limsuplt2  46525  liminfreuzlem  46574  liminfltlem  46576  liminflimsupclim  46579  xlimmnfmpt  46615  xlimpnfmpt  46616  fourierdlem73  46951  fourierdlem83  46961  meaiuninc3v  47256  ovolval2  47416  cfsetsnfsetfo  47855  dfaimafn  47960  iccelpart  48240  sprsymrelf  48302  sprsymrelfo  48304  nprmmul1  48334  nprmmul3  48336  fmtnoprmfac1  48375  fmtnoprmfac2  48377  fmtnofac2lem  48378  dfeven2  48472  dfodd3  48473  dfvopnbgr2  48676  usgrgrtrirex  48773  stgredgiun  48781  uspgrsprfo  48971  elbigo2  49389  rrxlinesc  49572  rrxlinec  49573  rrx2line  49577  rrx2vlinest  49578  itsclquadeu  49614