Theorem rexbidva 3160

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  rexbidv  3162  2rexbiia  3199  2rexbidva  3201  rexeqbidva  3303  frinxp  5707  onfr  6356  dfimafn  6896  funimass4  6898  fliftel  7257  fliftf  7263  isomin  7285  f1oiso  7299  releldm2  7989  oaass  8489  eldifsucnn  8593  cofonr  8603  naddunif  8622  qsinxp  8733  qliftel  8740  fimaxg  9190  ordunifi  9193  supisolem  9380  fiming  9406  wemapwe  9609  ttrcltr  9628  ttrclse  9639  frmin  9664  cflim2  10176  cfsmolem  10183  alephsing  10189  brdom7disj  10444  brdom6disj  10445  alephreg  10496  nqereu  10843  1idpr  10943  map2psrpr  11024  axsup  11212  rereccl  11864  sup3  12104  infm3  12106  supadd  12115  creur  12144  creui  12145  nndiv  12214  nnrecl  12426  rpnnen1lem2  12918  rpnnen1lem1  12919  rpnnen1lem3  12920  rpnnen1lem5  12922  supxrbnd1  13264  supxrbnd2  13265  supxrbnd  13271  rabssnn0fi  13939  mptnn0fsupp  13950  expnlbnd  14186  wrdl3s3  14915  limsuplt  15432  clim2  15457  clim2c  15458  clim0c  15460  ello12  15469  elo12  15480  rlimresb  15518  climabs0  15538  sumeq2ii  15646  mertens  15842  prodeq2ii  15867  zprod  15893  nndivides  16222  alzdvds  16280  oddm1even  16303  oddnn02np1  16308  oddge22np1  16309  evennn02n  16310  evennn2n  16311  divalglem4  16356  divalgb  16364  modremain  16368  modprmn0modprm0  16769  vdwlem6  16948  vdwlem11  16953  vdw  16956  ramval  16970  imasleval  17496  dfiso3  17731  fullestrcsetc  18108  fullsetcestrc  18123  isipodrs  18494  ipodrsfi  18496  gsumpropd2lem  18638  mndpropd  18718  grppropd  18918  qus0subgbas  19164  conjnmzb  19219  symgextfo  19388  symgfixfo  19405  sylow1lem2  19565  sylow3lem1  19593  sylow3lem3  19595  lsmelvalm  19617  lsmass  19635  iscyg3  19852  ghmcyg  19862  cycsubgcyg  19867  pgpfac1lem2  20043  pgpfac1lem4  20046  ablfac2  20057  dvdsr02  20343  crngunit  20349  dvdsrpropd  20387  rngqiprngimfo  21291  lpigen  21325  pzriprnglem10  21480  znunit  21553  elfilspd  21793  psdmul  22142  scmatmats  22486  symgmatr01  22629  isclo  23062  iscnp3  23219  lmbrf  23235  cncnp  23255  lmss  23273  isnrm2  23333  cmpfi  23383  1stcfb  23420  1stccnp  23437  ptrescn  23614  txkgen  23627  xkoinjcn  23662  trfil3  23863  fmid  23935  lmflf  23980  txflf  23981  ptcmplem3  24029  tsmsf1o  24120  ucnprima  24256  metrest  24499  metcnp  24516  metcnp2  24517  txmetcnp  24522  metuel2  24540  metustbl  24541  psmetutop  24542  metucn  24546  evth2  24937  lmmbrf  25239  iscfil2  25243  fmcfil  25249  iscau2  25254  iscau4  25256  iscauf  25257  caucfil  25260  iscmet3lem3  25267  cfilresi  25272  causs  25275  lmclim  25280  ivth2  25432  ovolfioo  25444  ovolficc  25445  ovolshftlem1  25486  ovolscalem1  25490  volsup2  25582  ismbf3d  25631  mbfaddlem  25637  mbfsup  25641  mbfinf  25642  itg2seq  25719  itg2gt0  25737  ellimc2  25854  ellimc3  25856  rolle  25967  cmvth  25968  mvth  25969  dvlip  25970  dvivth  25987  lhop1lem  25990  deg1ldg  26067  ulm2  26363  ulmdvlem3  26380  dcubic  26823  mcubic  26824  cubic2  26825  rlimcnp  26942  ftalem3  27052  isppw2  27092  lgsquadlem2  27358  2lgslem1a  27368  dchrmusumlema  27470  dchrisum0lema  27491  cofcutr  27930  lrrecfr  27949  addsrid  27970  addscom  27972  addsuniflem  28007  addsass  28011  addbday  28024  negsunif  28061  mulsrid  28119  mulsasslem3  28171  n0s0suc  28348  z12sge0  28489  elreno2  28501  renegscl  28504  readdscl  28505  remulscllem2  28507  remulscl  28508  tglowdim2l  28732  mirreu3  28736  oppcom  28826  iscgra1  28892  axsegcon  29010  axpasch  29024  axcontlem7  29053  usgr2pth0  29848  usgr2wspthon  30051  elwwlks2  30052  elwspths2spth  30053  rusgrnumwwlks  30060  clwwlkfo  30135  eclclwwlkn1  30160  eucrctshift  30328  fusgreg2wsp  30421  nmobndi  30861  nmounbi  30862  nmoo0  30877  h2hcau  31065  h2hlm  31066  shsel3  31401  pjhtheu2  31502  chscllem2  31724  adjbdln  32169  branmfn  32191  pjimai  32262  chrelati  32450  cdj3lem3  32524  cdj3lem3b  32526  dfimafnf  32724  ofpreima  32753  isarchi2  33261  submarchi  33262  archirng  33264  archiabl  33274  isarchiofld  33275  ellspds  33443  dvdsruasso2  33461  lsmssass  33477  grplsm0l  33478  fedgmullem2  33790  elirng  33846  zarcls  34034  ordtconnlem1  34084  lmdvg  34113  esumfsup  34230  dya2icoseg2  34438  eulerpartlemgh  34538  ballotlemodife  34658  ballotlemsima  34676  nummin  35252  erdszelem10  35398  iscvm  35457  wsuclem  36021  seglelin  36314  outsideofeu  36329  opnrebl  36518  opnrebl2  36519  filnetlem4  36579  bj-finsumval0  37615  phpreu  37939  ptrest  37954  poimirlem3  37958  poimirlem4  37959  poimirlem17  37972  poimirlem26  37981  poimirlem27  37982  broucube  37989  mblfinlem1  37992  lmclim2  38093  caures  38095  isbnd3b  38120  heiborlem7  38152  heiborlem10  38155  rrncmslem  38167  isdrngo2  38293  erimeq2  39098  prter3  39342  islshpsm  39440  lsatfixedN  39469  lrelat  39474  eqlkr2  39560  lshpkrlem1  39570  lfl1dim  39581  eqlkr4  39625  ishlat3N  39814  hlsupr2  39847  hlrelat5N  39861  hlrelat  39862  cvrval5  39875  cvrat42  39904  athgt  39916  3dim0  39917  islln3  39970  llnexatN  39981  islpln3  39993  islvol3  40036  islvol5  40039  isline4N  40237  polval2N  40366  4atex3  40541  cdleme0ex2N  40684  cdlemefrs29cpre1  40858  cdlemb3  41066  cdlemg33c  41168  cdlemg33e  41170  dia1dim2  41522  cdlemm10N  41578  dib1dim2  41628  diclspsn  41654  dih1dimatlem  41789  dihatexv2  41799  djhcvat42  41875  dihjat1lem  41888  dvh4dimat  41898  dvh2dimatN  41900  lcfrlem9  42010  mapdval4N  42092  mapdcv  42120  ef11d  42785  cxp112d  42787  cxp111d  42788  sn-sup3d  42951  fimgmcyc  42993  infdesc  43090  elrfirn  43141  elrfirn2  43142  mrefg3  43154  diophin  43218  diophun  43219  diophren  43259  rmxycomplete  43363  wepwsolem  43488  fnwe2lem2  43497  islssfg  43516  unielss  43664  onmaxnelsup  43669  onsupnmax  43674  onsupeqnmax  43693  tfsconcat0i  43791  ntrneineine0lem  44528  ntrneineine1lem  44529  ntrneiel2  44531  extoimad  44609  grumnudlem  44730  modelac8prim  45437  supsubc  45801  infxrbnd2  45816  supminfxr  45910  evthiccabs  45944  elicores  45981  clim2f  46082  clim2cf  46096  clim0cf  46100  clim2f2  46116  limsupub  46150  limsupmnflem  46166  limsupre2lem  46170  limsuplt2  46199  liminfreuzlem  46248  liminfltlem  46250  liminflimsupclim  46253  xlimmnfmpt  46289  xlimpnfmpt  46290  fourierdlem73  46625  fourierdlem83  46635  meaiuninc3v  46930  ovolval2  47090  cfsetsnfsetfo  47520  dfaimafn  47625  iccelpart  47905  sprsymrelf  47967  sprsymrelfo  47969  nprmmul1  47999  nprmmul3  48001  fmtnoprmfac1  48040  fmtnoprmfac2  48042  fmtnofac2lem  48043  dfeven2  48137  dfodd3  48138  dfvopnbgr2  48341  usgrgrtrirex  48438  stgredgiun  48446  uspgrsprfo  48636  elbigo2  49040  rrxlinesc  49223  rrxlinec  49224  rrx2line  49228  rrx2vlinest  49229  itsclquadeu  49265