Theorem rexbidva 3177

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

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

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 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  rexbidv  3179  2rexbiia  3216  2rexbidva  3218  rexeqbidva  3329  frinxp  5756  onfr  6400  dfimafn  6951  funimass4  6953  fliftel  7301  fliftf  7307  isomin  7329  f1oiso  7343  releldm2  8024  oaass  8557  eldifsucnn  8659  cofonr  8669  naddunif  8688  qsinxp  8783  qliftel  8790  fimaxg  9286  ordunifi  9289  supisolem  9464  fiming  9489  wemapwe  9688  ttrcltr  9707  ttrclse  9718  frmin  9740  cflim2  10254  cfsmolem  10261  alephsing  10267  brdom7disj  10522  brdom6disj  10523  alephreg  10573  nqereu  10920  1idpr  11020  map2psrpr  11101  axsup  11285  rereccl  11928  sup3  12167  infm3  12169  supadd  12178  creur  12202  creui  12203  nndiv  12254  nnrecl  12466  rpnnen1lem2  12957  rpnnen1lem1  12958  rpnnen1lem3  12959  rpnnen1lem5  12961  supxrbnd1  13296  supxrbnd2  13297  supxrbnd  13303  rabssnn0fi  13947  mptnn0fsupp  13958  expnlbnd  14192  wrdl3s3  14909  limsuplt  15419  clim2  15444  clim2c  15445  clim0c  15447  ello12  15456  elo12  15467  rlimresb  15505  climabs0  15525  sumeq2ii  15635  mertens  15828  prodeq2ii  15853  zprod  15877  nndivides  16203  alzdvds  16259  oddm1even  16282  oddnn02np1  16287  oddge22np1  16288  evennn02n  16289  evennn2n  16290  divalglem4  16335  divalgb  16343  modremain  16347  modprmn0modprm0  16736  vdwlem6  16915  vdwlem11  16920  vdw  16923  ramval  16937  imasleval  17483  dfiso3  17716  fullestrcsetc  18099  fullsetcestrc  18114  isipodrs  18486  ipodrsfi  18488  gsumpropd2lem  18594  mndpropd  18646  grppropd  18833  qus0subgbas  19069  conjnmzb  19121  symgextfo  19283  symgfixfo  19300  sylow1lem2  19460  sylow3lem1  19488  sylow3lem3  19490  lsmelvalm  19512  lsmass  19530  iscyg3  19746  ghmcyg  19756  cycsubgcyg  19761  pgpfac1lem2  19937  pgpfac1lem4  19940  ablfac2  19951  dvdsr02  20175  crngunit  20181  dvdsrpropd  20219  lpigen  20881  znunit  21103  elfilspd  21342  scmatmats  21995  symgmatr01  22138  isclo  22573  iscnp3  22730  lmbrf  22746  cncnp  22766  lmss  22784  isnrm2  22844  cmpfi  22894  1stcfb  22931  1stccnp  22948  ptrescn  23125  txkgen  23138  xkoinjcn  23173  trfil3  23374  fmid  23446  lmflf  23491  txflf  23492  ptcmplem3  23540  tsmsf1o  23631  ucnprima  23769  metrest  24015  metcnp  24032  metcnp2  24033  txmetcnp  24038  metuel2  24056  metustbl  24057  psmetutop  24058  metucn  24062  evth2  24458  lmmbrf  24761  iscfil2  24765  fmcfil  24771  iscau2  24776  iscau4  24778  iscauf  24779  caucfil  24782  iscmet3lem3  24789  cfilresi  24794  causs  24797  lmclim  24802  ivth2  24954  ovolfioo  24966  ovolficc  24967  ovolshftlem1  25008  ovolscalem1  25012  volsup2  25104  ismbf3d  25153  mbfaddlem  25159  mbfsup  25163  mbfinf  25164  itg2seq  25242  itg2gt0  25260  ellimc2  25376  ellimc3  25378  rolle  25489  cmvth  25490  mvth  25491  dvlip  25492  dvivth  25509  lhop1lem  25512  deg1ldg  25592  ulm2  25879  ulmdvlem3  25896  dcubic  26331  mcubic  26332  cubic2  26333  rlimcnp  26450  ftalem3  26559  isppw2  26599  lgsquadlem2  26864  2lgslem1a  26874  dchrmusumlema  26976  dchrisum0lema  26997  cofcutr  27391  lrrecfr  27407  addsrid  27428  addscom  27430  addsuniflem  27464  addsass  27468  negsunif  27509  mulsrid  27549  mulsasslem3  27600  tglowdim2l  27881  mirreu3  27885  oppcom  27975  iscgra1  28041  axsegcon  28165  axpasch  28179  axcontlem7  28208  usgr2pth0  29002  usgr2wspthon  29199  elwwlks2  29200  elwspths2spth  29201  rusgrnumwwlks  29208  clwwlkfo  29283  eclclwwlkn1  29308  eucrctshift  29476  fusgreg2wsp  29569  nmobndi  30006  nmounbi  30007  nmoo0  30022  h2hcau  30210  h2hlm  30211  shsel3  30546  pjhtheu2  30647  chscllem2  30869  adjbdln  31314  branmfn  31336  pjimai  31407  chrelati  31595  cdj3lem3  31669  cdj3lem3b  31671  dfimafnf  31838  ofpreima  31868  isarchi2  32309  submarchi  32310  archirng  32312  archiabl  32322  isarchiofld  32404  ellspds  32450  lsmssass  32477  grplsm0l  32478  fedgmullem2  32660  elirng  32695  zarcls  32792  ordtconnlem1  32842  lmdvg  32871  esumfsup  33006  dya2icoseg2  33215  eulerpartlemgh  33315  ballotlemodife  33434  ballotlemsima  33452  nummin  34032  erdszelem10  34129  iscvm  34188  wsuclem  34735  seglelin  35026  outsideofeu  35041  gg-cmvth  35119  opnrebl  35143  opnrebl2  35144  filnetlem4  35204  bj-finsumval0  36104  phpreu  36410  ptrest  36425  poimirlem3  36429  poimirlem4  36430  poimirlem17  36443  poimirlem26  36452  poimirlem27  36453  broucube  36460  mblfinlem1  36463  lmclim2  36564  caures  36566  isbnd3b  36591  heiborlem7  36623  heiborlem10  36626  rrncmslem  36638  isdrngo2  36764  erimeq2  37486  prter3  37690  islshpsm  37788  lsatfixedN  37817  lrelat  37822  eqlkr2  37908  lshpkrlem1  37918  lfl1dim  37929  eqlkr4  37973  ishlat3N  38162  hlsupr2  38196  hlrelat5N  38210  hlrelat  38211  cvrval5  38224  cvrat42  38253  athgt  38265  3dim0  38266  islln3  38319  llnexatN  38330  islpln3  38342  islvol3  38385  islvol5  38388  isline4N  38586  polval2N  38715  4atex3  38890  cdleme0ex2N  39033  cdlemefrs29cpre1  39207  cdlemb3  39415  cdlemg33c  39517  cdlemg33e  39519  dia1dim2  39871  cdlemm10N  39927  dib1dim2  39977  diclspsn  40003  dih1dimatlem  40138  dihatexv2  40148  djhcvat42  40224  dihjat1lem  40237  dvh4dimat  40247  dvh2dimatN  40249  lcfrlem9  40359  mapdval4N  40441  mapdcv  40469  infdesc  41329  elrfirn  41366  elrfirn2  41367  mrefg3  41379  diophin  41443  diophun  41444  diophren  41484  rmxycomplete  41589  wepwsolem  41717  fnwe2lem2  41726  islssfg  41745  unielss  41900  onmaxnelsup  41905  onsupnmax  41910  onsupeqnmax  41929  tfsconcat0i  42028  ntrneineine0lem  42767  ntrneineine1lem  42768  ntrneiel2  42770  extoimad  42849  grumnudlem  42977  supsubc  43998  infxrbnd2  44014  supminfxr  44109  evthiccabs  44144  elicores  44181  clim2f  44287  clim2cf  44301  clim0cf  44305  clim2f2  44321  limsupub  44355  limsupmnflem  44371  limsupre2lem  44375  limsuplt2  44404  liminfreuzlem  44453  liminfltlem  44455  liminflimsupclim  44458  xlimmnfmpt  44494  xlimpnfmpt  44495  fourierdlem73  44830  fourierdlem83  44840  meaiuninc3v  45135  ovolval2  45295  cfsetsnfsetfo  45705  dfaimafn  45808  iccelpart  46036  sprsymrelf  46098  sprsymrelfo  46100  fmtnoprmfac1  46168  fmtnoprmfac2  46170  fmtnofac2lem  46171  dfeven2  46252  dfodd3  46253  isomuspgrlem2d  46434  uspgrsprfo  46461  rngqiprngimfo  46715  elbigo2  47140  rrxlinesc  47323  rrxlinec  47324  rrx2line  47328  rrx2vlinest  47329  itsclquadeu  47365