Theorem rexbidva 3161

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∈ wcel 2119  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3064

This theorem is referenced by:  rexbidv  3163  2rexbiia  3200  2rexbidva  3202  rexeqbidva  3304  frinxp  5701  onfr  6349  dfimafn  6889  funimass4  6891  fliftel  7253  fliftf  7259  isomin  7281  f1oiso  7295  releldm2  7985  oaass  8486  eldifsucnn  8590  cofonr  8600  naddunif  8619  qsinxp  8730  qliftel  8737  fimaxg  9187  ordunifi  9190  supisolem  9377  fiming  9403  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  21294  lpigen  21328  pzriprnglem10  21465  znunit  21538  elfilspd  21778  psdmul  22154  scmatmats  22494  symgmatr01  22637  isclo  23070  iscnp3  23227  lmbrf  23243  cncnp  23263  lmss  23281  isnrm2  23341  cmpfi  23391  1stcfb  23428  1stccnp  23445  ptrescn  23622  txkgen  23635  xkoinjcn  23670  trfil3  23871  fmid  23943  lmflf  23988  txflf  23989  ptcmplem3  24037  tsmsf1o  24128  ucnprima  24264  metrest  24507  metcnp  24524  metcnp2  24525  txmetcnp  24530  metuel2  24548  metustbl  24549  psmetutop  24550  metucn  24554  evth2  24945  lmmbrf  25247  iscfil2  25251  fmcfil  25257  iscau2  25262  iscau4  25264  iscauf  25265  caucfil  25268  iscmet3lem3  25275  cfilresi  25280  causs  25283  lmclim  25288  ivth2  25440  ovolfioo  25452  ovolficc  25453  ovolshftlem1  25494  ovolscalem1  25498  volsup2  25590  ismbf3d  25639  mbfaddlem  25645  mbfsup  25649  mbfinf  25650  itg2seq  25727  itg2gt0  25745  ellimc2  25862  ellimc3  25864  rolle  25975  cmvth  25976  mvth  25977  dvlip  25978  dvivth  25995  lhop1lem  25998  deg1ldg  26075  ulm2  26368  ulmdvlem3  26385  dcubic  26828  mcubic  26829  cubic2  26830  rlimcnp  26947  ftalem3  27056  isppw2  27096  lgsquadlem2  27362  2lgslem1a  27372  dchrmusumlema  27474  dchrisum0lema  27495  cofcutr  27934  lrrecfr  27953  addsrid  27974  addscom  27976  addsuniflem  28011  addsass  28015  addbday  28028  negsunif  28065  mulsrid  28123  mulsasslem3  28175  n0s0suc  28352  z12sge0  28493  elreno2  28505  renegscl  28508  readdscl  28509  remulscllem2  28511  remulscl  28512  tglowdim2l  28736  mirreu3  28740  oppcom  28830  iscgra1  28896  axsegcon  29014  axpasch  29028  axcontlem7  29057  usgr2pth0  29851  usgr2wspthon  30054  elwwlks2  30055  elwspths2spth  30056  rusgrnumwwlks  30063  clwwlkfo  30138  eclclwwlkn1  30163  eucrctshift  30331  fusgreg2wsp  30424  nmobndi  30864  nmounbi  30865  nmoo0  30880  h2hcau  31068  h2hlm  31069  shsel3  31404  pjhtheu2  31505  chscllem2  31727  adjbdln  32172  branmfn  32194  pjimai  32265  chrelati  32453  cdj3lem3  32527  cdj3lem3b  32529  dfimafnf  32728  ofpreima  32757  isarchi2  33266  submarchi  33267  archirng  33269  archiabl  33279  isarchiofld  33280  ellspds  33451  dvdsruasso2  33469  lsmssass  33485  grplsm0l  33486  fedgmullem2  33814  elirng  33870  zarcls  34058  ordtconnlem1  34108  lmdvg  34137  esumfsup  34254  dya2icoseg2  34462  eulerpartlemgh  34562  ballotlemodife  34682  ballotlemsima  34700  nummin  35274  erdszelem10  35428  iscvm  35487  wsuclem  36051  seglelin  36344  outsideofeu  36359  opnrebl  36548  opnrebl2  36549  filnetlem4  36609  bj-finsumval0  37645  phpreu  37971  ptrest  37986  poimirlem3  37990  poimirlem4  37991  poimirlem17  38004  poimirlem26  38013  poimirlem27  38014  broucube  38021  mblfinlem1  38024  lmclim2  38125  caures  38127  isbnd3b  38152  heiborlem7  38184  heiborlem10  38187  rrncmslem  38199  isdrngo2  38325  erimeq2  39130  prter3  39374  islshpsm  39472  lsatfixedN  39501  lrelat  39506  eqlkr2  39592  lshpkrlem1  39602  lfl1dim  39613  eqlkr4  39657  ishlat3N  39846  hlsupr2  39879  hlrelat5N  39893  hlrelat  39894  cvrval5  39907  cvrat42  39936  athgt  39948  3dim0  39949  islln3  40002  llnexatN  40013  islpln3  40025  islvol3  40068  islvol5  40071  isline4N  40269  polval2N  40398  4atex3  40573  cdleme0ex2N  40716  cdlemefrs29cpre1  40890  cdlemb3  41098  cdlemg33c  41200  cdlemg33e  41202  dia1dim2  41554  cdlemm10N  41610  dib1dim2  41660  diclspsn  41686  dih1dimatlem  41821  dihatexv2  41831  djhcvat42  41907  dihjat1lem  41920  dvh4dimat  41930  dvh2dimatN  41932  lcfrlem9  42042  mapdval4N  42124  mapdcv  42152  ef11d  42816  cxp112d  42818  cxp111d  42819  sn-sup3d  42982  fimgmcyc  43020  infdesc  43093  elrfirn  43144  elrfirn2  43145  mrefg3  43157  diophin  43221  diophun  43222  diophren  43258  rmxycomplete  43362  wepwsolem  43487  fnwe2lem2  43496  islssfg  43515  unielss  43663  onmaxnelsup  43668  onsupnmax  43673  onsupeqnmax  43692  tfsconcat0i  43790  ntrneineine0lem  44527  ntrneineine1lem  44528  ntrneiel2  44530  extoimad  44608  grumnudlem  44729  modelac8prim  45436  supsubc  45798  infxrbnd2  45813  supminfxr  45907  evthiccabs  45941  elicores  45978  clim2f  46079  clim2cf  46093  clim0cf  46097  clim2f2  46113  limsupub  46147  limsupmnflem  46163  limsupre2lem  46167  limsuplt2  46196  liminfreuzlem  46245  liminfltlem  46247  liminflimsupclim  46250  xlimmnfmpt  46286  xlimpnfmpt  46287  fourierdlem73  46622  fourierdlem83  46632  meaiuninc3v  46927  ovolval2  47087  cfsetsnfsetfo  47523  dfaimafn  47628  iccelpart  47908  sprsymrelf  47970  sprsymrelfo  47972  nprmmul1  48002  nprmmul3  48004  fmtnoprmfac1  48043  fmtnoprmfac2  48045  fmtnofac2lem  48046  dfeven2  48140  dfodd3  48141  dfvopnbgr2  48344  usgrgrtrirex  48441  stgredgiun  48449  uspgrsprfo  48639  elbigo2  49043  rrxlinesc  49226  rrxlinec  49227  rrx2line  49231  rrx2vlinest  49232  itsclquadeu  49268