Theorem rexbidva 3156

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

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

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 3055

This theorem is referenced by:  rexbidv  3158  2rexbiia  3199  2rexbidva  3201  rexeqbidva  3308  frinxp  5724  onfr  6374  dfimafn  6926  funimass4  6928  fliftel  7287  fliftf  7293  isomin  7315  f1oiso  7329  releldm2  8025  oaass  8528  eldifsucnn  8631  cofonr  8641  naddunif  8660  qsinxp  8769  qliftel  8776  fimaxg  9241  ordunifi  9244  supisolem  9432  fiming  9458  wemapwe  9657  ttrcltr  9676  ttrclse  9687  frmin  9709  cflim2  10223  cfsmolem  10230  alephsing  10236  brdom7disj  10491  brdom6disj  10492  alephreg  10542  nqereu  10889  1idpr  10989  map2psrpr  11070  axsup  11256  rereccl  11907  sup3  12147  infm3  12149  supadd  12158  creur  12187  creui  12188  nndiv  12239  nnrecl  12447  rpnnen1lem2  12943  rpnnen1lem1  12944  rpnnen1lem3  12945  rpnnen1lem5  12947  supxrbnd1  13288  supxrbnd2  13289  supxrbnd  13295  rabssnn0fi  13958  mptnn0fsupp  13969  expnlbnd  14205  wrdl3s3  14935  limsuplt  15452  clim2  15477  clim2c  15478  clim0c  15480  ello12  15489  elo12  15500  rlimresb  15538  climabs0  15558  sumeq2ii  15666  mertens  15859  prodeq2ii  15884  zprod  15910  nndivides  16239  alzdvds  16297  oddm1even  16320  oddnn02np1  16325  oddge22np1  16326  evennn02n  16327  evennn2n  16328  divalglem4  16373  divalgb  16381  modremain  16385  modprmn0modprm0  16785  vdwlem6  16964  vdwlem11  16969  vdw  16972  ramval  16986  imasleval  17511  dfiso3  17742  fullestrcsetc  18119  fullsetcestrc  18134  isipodrs  18503  ipodrsfi  18505  gsumpropd2lem  18613  mndpropd  18693  grppropd  18890  qus0subgbas  19137  conjnmzb  19192  symgextfo  19359  symgfixfo  19376  sylow1lem2  19536  sylow3lem1  19564  sylow3lem3  19566  lsmelvalm  19588  lsmass  19606  iscyg3  19823  ghmcyg  19833  cycsubgcyg  19838  pgpfac1lem2  20014  pgpfac1lem4  20017  ablfac2  20028  dvdsr02  20288  crngunit  20294  dvdsrpropd  20332  rngqiprngimfo  21218  lpigen  21252  pzriprnglem10  21407  znunit  21480  elfilspd  21719  psdmul  22060  scmatmats  22405  symgmatr01  22548  isclo  22981  iscnp3  23138  lmbrf  23154  cncnp  23174  lmss  23192  isnrm2  23252  cmpfi  23302  1stcfb  23339  1stccnp  23356  ptrescn  23533  txkgen  23546  xkoinjcn  23581  trfil3  23782  fmid  23854  lmflf  23899  txflf  23900  ptcmplem3  23948  tsmsf1o  24039  ucnprima  24176  metrest  24419  metcnp  24436  metcnp2  24437  txmetcnp  24442  metuel2  24460  metustbl  24461  psmetutop  24462  metucn  24466  evth2  24866  lmmbrf  25169  iscfil2  25173  fmcfil  25179  iscau2  25184  iscau4  25186  iscauf  25187  caucfil  25190  iscmet3lem3  25197  cfilresi  25202  causs  25205  lmclim  25210  ivth2  25363  ovolfioo  25375  ovolficc  25376  ovolshftlem1  25417  ovolscalem1  25421  volsup2  25513  ismbf3d  25562  mbfaddlem  25568  mbfsup  25572  mbfinf  25573  itg2seq  25650  itg2gt0  25668  ellimc2  25785  ellimc3  25787  rolle  25901  cmvth  25902  cmvthOLD  25903  mvth  25904  dvlip  25905  dvivth  25922  lhop1lem  25925  deg1ldg  26004  ulm2  26301  ulmdvlem3  26318  dcubic  26763  mcubic  26764  cubic2  26765  rlimcnp  26882  ftalem3  26992  isppw2  27032  lgsquadlem2  27299  2lgslem1a  27309  dchrmusumlema  27411  dchrisum0lema  27432  cofcutr  27839  lrrecfr  27857  addsrid  27878  addscom  27880  addsuniflem  27915  addsass  27919  addsbday  27931  negsunif  27968  mulsrid  28023  mulsasslem3  28075  n0s0suc  28241  zs12ge0  28349  renegscl  28356  readdscl  28357  remulscllem2  28359  remulscl  28360  tglowdim2l  28584  mirreu3  28588  oppcom  28678  iscgra1  28744  axsegcon  28861  axpasch  28875  axcontlem7  28904  usgr2pth0  29702  usgr2wspthon  29902  elwwlks2  29903  elwspths2spth  29904  rusgrnumwwlks  29911  clwwlkfo  29986  eclclwwlkn1  30011  eucrctshift  30179  fusgreg2wsp  30272  nmobndi  30711  nmounbi  30712  nmoo0  30727  h2hcau  30915  h2hlm  30916  shsel3  31251  pjhtheu2  31352  chscllem2  31574  adjbdln  32019  branmfn  32041  pjimai  32112  chrelati  32300  cdj3lem3  32374  cdj3lem3b  32376  dfimafnf  32567  ofpreima  32596  isarchi2  33146  submarchi  33147  archirng  33149  archiabl  33159  isarchiofld  33302  ellspds  33346  dvdsruasso2  33364  lsmssass  33380  grplsm0l  33381  fedgmullem2  33633  elirng  33688  zarcls  33871  ordtconnlem1  33921  lmdvg  33950  esumfsup  34067  dya2icoseg2  34276  eulerpartlemgh  34376  ballotlemodife  34496  ballotlemsima  34514  nummin  35088  erdszelem10  35194  iscvm  35253  wsuclem  35820  seglelin  36111  outsideofeu  36126  opnrebl  36315  opnrebl2  36316  filnetlem4  36376  bj-finsumval0  37280  phpreu  37605  ptrest  37620  poimirlem3  37624  poimirlem4  37625  poimirlem17  37638  poimirlem26  37647  poimirlem27  37648  broucube  37655  mblfinlem1  37658  lmclim2  37759  caures  37761  isbnd3b  37786  heiborlem7  37818  heiborlem10  37821  rrncmslem  37833  isdrngo2  37959  erimeq2  38677  prter3  38882  islshpsm  38980  lsatfixedN  39009  lrelat  39014  eqlkr2  39100  lshpkrlem1  39110  lfl1dim  39121  eqlkr4  39165  ishlat3N  39354  hlsupr2  39388  hlrelat5N  39402  hlrelat  39403  cvrval5  39416  cvrat42  39445  athgt  39457  3dim0  39458  islln3  39511  llnexatN  39522  islpln3  39534  islvol3  39577  islvol5  39580  isline4N  39778  polval2N  39907  4atex3  40082  cdleme0ex2N  40225  cdlemefrs29cpre1  40399  cdlemb3  40607  cdlemg33c  40709  cdlemg33e  40711  dia1dim2  41063  cdlemm10N  41119  dib1dim2  41169  diclspsn  41195  dih1dimatlem  41330  dihatexv2  41340  djhcvat42  41416  dihjat1lem  41429  dvh4dimat  41439  dvh2dimatN  41441  lcfrlem9  41551  mapdval4N  41633  mapdcv  41661  ef11d  42334  cxp112d  42336  cxp111d  42337  sn-sup3d  42487  fimgmcyc  42529  infdesc  42638  elrfirn  42690  elrfirn2  42691  mrefg3  42703  diophin  42767  diophun  42768  diophren  42808  rmxycomplete  42913  wepwsolem  43038  fnwe2lem2  43047  islssfg  43066  unielss  43214  onmaxnelsup  43219  onsupnmax  43224  onsupeqnmax  43243  tfsconcat0i  43341  ntrneineine0lem  44079  ntrneineine1lem  44080  ntrneiel2  44082  extoimad  44160  grumnudlem  44281  modelac8prim  44989  supsubc  45356  infxrbnd2  45372  supminfxr  45467  evthiccabs  45501  elicores  45538  clim2f  45641  clim2cf  45655  clim0cf  45659  clim2f2  45675  limsupub  45709  limsupmnflem  45725  limsupre2lem  45729  limsuplt2  45758  liminfreuzlem  45807  liminfltlem  45809  liminflimsupclim  45812  xlimmnfmpt  45848  xlimpnfmpt  45849  fourierdlem73  46184  fourierdlem83  46194  meaiuninc3v  46489  ovolval2  46649  cfsetsnfsetfo  47065  dfaimafn  47170  iccelpart  47438  sprsymrelf  47500  sprsymrelfo  47502  fmtnoprmfac1  47570  fmtnoprmfac2  47572  fmtnofac2lem  47573  dfeven2  47654  dfodd3  47655  dfvopnbgr2  47857  usgrgrtrirex  47953  stgredgiun  47961  uspgrsprfo  48140  elbigo2  48545  rrxlinesc  48728  rrxlinec  48729  rrx2line  48733  rrx2vlinest  48734  itsclquadeu  48770