Theorem rexbidva 3169

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∈ wcel 2106  ∃wrex 3069

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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3070

This theorem is referenced by:  rexbidv  3171  2rexbiia  3205  2rexbidva  3207  rexeqbidva  3320  frinxp  5719  onfr  6361  dfimafn  6910  funimass4  6912  fliftel  7259  fliftf  7265  isomin  7287  f1oiso  7301  releldm2  7980  oaass  8513  eldifsucnn  8615  cofonr  8625  naddunif  8644  qsinxp  8739  qliftel  8746  fimaxg  9241  ordunifi  9244  supisolem  9418  fiming  9443  wemapwe  9642  ttrcltr  9661  ttrclse  9672  frmin  9694  cflim2  10208  cfsmolem  10215  alephsing  10221  brdom7disj  10476  brdom6disj  10477  alephreg  10527  nqereu  10874  1idpr  10974  map2psrpr  11055  axsup  11239  rereccl  11882  sup3  12121  infm3  12123  supadd  12132  creur  12156  creui  12157  nndiv  12208  nnrecl  12420  rpnnen1lem2  12911  rpnnen1lem1  12912  rpnnen1lem3  12913  rpnnen1lem5  12915  supxrbnd1  13250  supxrbnd2  13251  supxrbnd  13257  rabssnn0fi  13901  mptnn0fsupp  13912  expnlbnd  14146  wrdl3s3  14863  limsuplt  15373  clim2  15398  clim2c  15399  clim0c  15401  ello12  15410  elo12  15421  rlimresb  15459  climabs0  15479  sumeq2ii  15589  mertens  15782  prodeq2ii  15807  zprod  15831  nndivides  16157  alzdvds  16213  oddm1even  16236  oddnn02np1  16241  oddge22np1  16242  evennn02n  16243  evennn2n  16244  divalglem4  16289  divalgb  16297  modremain  16301  modprmn0modprm0  16690  vdwlem6  16869  vdwlem11  16874  vdw  16877  ramval  16891  imasleval  17437  dfiso3  17670  fullestrcsetc  18053  fullsetcestrc  18068  isipodrs  18440  ipodrsfi  18442  gsumpropd2lem  18548  mndpropd  18595  grppropd  18779  conjnmzb  19057  symgextfo  19218  symgfixfo  19235  sylow1lem2  19395  sylow3lem1  19423  sylow3lem3  19425  lsmelvalm  19447  lsmass  19465  iscyg3  19677  ghmcyg  19687  cycsubgcyg  19692  pgpfac1lem2  19868  pgpfac1lem4  19871  ablfac2  19882  dvdsr02  20099  crngunit  20105  dvdsrpropd  20141  lpigen  20785  znunit  21007  elfilspd  21246  scmatmats  21897  symgmatr01  22040  isclo  22475  iscnp3  22632  lmbrf  22648  cncnp  22668  lmss  22686  isnrm2  22746  cmpfi  22796  1stcfb  22833  1stccnp  22850  ptrescn  23027  txkgen  23040  xkoinjcn  23075  trfil3  23276  fmid  23348  lmflf  23393  txflf  23394  ptcmplem3  23442  tsmsf1o  23533  ucnprima  23671  metrest  23917  metcnp  23934  metcnp2  23935  txmetcnp  23940  metuel2  23958  metustbl  23959  psmetutop  23960  metucn  23964  evth2  24360  lmmbrf  24663  iscfil2  24667  fmcfil  24673  iscau2  24678  iscau4  24680  iscauf  24681  caucfil  24684  iscmet3lem3  24691  cfilresi  24696  causs  24699  lmclim  24704  ivth2  24856  ovolfioo  24868  ovolficc  24869  ovolshftlem1  24910  ovolscalem1  24914  volsup2  25006  ismbf3d  25055  mbfaddlem  25061  mbfsup  25065  mbfinf  25066  itg2seq  25144  itg2gt0  25162  ellimc2  25278  ellimc3  25280  rolle  25391  cmvth  25392  mvth  25393  dvlip  25394  dvivth  25411  lhop1lem  25414  deg1ldg  25494  ulm2  25781  ulmdvlem3  25798  dcubic  26233  mcubic  26234  cubic2  26235  rlimcnp  26352  ftalem3  26461  isppw2  26501  lgsquadlem2  26766  2lgslem1a  26776  dchrmusumlema  26878  dchrisum0lema  26899  cofcutr  27286  lrrecfr  27298  addsrid  27319  addscom  27321  addsunif  27353  addsass  27356  negsunif  27393  mulsrid  27420  mulslid  27421  tglowdim2l  27655  mirreu3  27659  oppcom  27749  iscgra1  27815  axsegcon  27939  axpasch  27953  axcontlem7  27982  usgr2pth0  28776  usgr2wspthon  28973  elwwlks2  28974  elwspths2spth  28975  rusgrnumwwlks  28982  clwwlkfo  29057  eclclwwlkn1  29082  eucrctshift  29250  fusgreg2wsp  29343  nmobndi  29780  nmounbi  29781  nmoo0  29796  h2hcau  29984  h2hlm  29985  shsel3  30320  pjhtheu2  30421  chscllem2  30643  adjbdln  31088  branmfn  31110  pjimai  31181  chrelati  31369  cdj3lem3  31443  cdj3lem3b  31445  dfimafnf  31617  ofpreima  31648  isarchi2  32091  submarchi  32092  archirng  32094  archiabl  32104  isarchiofld  32183  ellspds  32229  lsmssass  32256  grplsm0l  32257  fedgmullem2  32412  elirng  32447  zarcls  32544  ordtconnlem1  32594  lmdvg  32623  esumfsup  32758  dya2icoseg2  32967  eulerpartlemgh  33067  ballotlemodife  33186  ballotlemsima  33204  nummin  33784  erdszelem10  33881  iscvm  33940  wsuclem  34486  seglelin  34777  outsideofeu  34792  opnrebl  34868  opnrebl2  34869  filnetlem4  34929  bj-finsumval0  35829  phpreu  36135  ptrest  36150  poimirlem3  36154  poimirlem4  36155  poimirlem17  36168  poimirlem26  36177  poimirlem27  36178  broucube  36185  mblfinlem1  36188  lmclim2  36290  caures  36292  isbnd3b  36317  heiborlem7  36349  heiborlem10  36352  rrncmslem  36364  isdrngo2  36490  erimeq2  37213  prter3  37417  islshpsm  37515  lsatfixedN  37544  lrelat  37549  eqlkr2  37635  lshpkrlem1  37645  lfl1dim  37656  eqlkr4  37700  ishlat3N  37889  hlsupr2  37923  hlrelat5N  37937  hlrelat  37938  cvrval5  37951  cvrat42  37980  athgt  37992  3dim0  37993  islln3  38046  llnexatN  38057  islpln3  38069  islvol3  38112  islvol5  38115  isline4N  38313  polval2N  38442  4atex3  38617  cdleme0ex2N  38760  cdlemefrs29cpre1  38934  cdlemb3  39142  cdlemg33c  39244  cdlemg33e  39246  dia1dim2  39598  cdlemm10N  39654  dib1dim2  39704  diclspsn  39730  dih1dimatlem  39865  dihatexv2  39875  djhcvat42  39951  dihjat1lem  39964  dvh4dimat  39974  dvh2dimatN  39976  lcfrlem9  40086  mapdval4N  40168  mapdcv  40196  infdesc  41039  elrfirn  41076  elrfirn2  41077  mrefg3  41089  diophin  41153  diophun  41154  diophren  41194  rmxycomplete  41299  wepwsolem  41427  fnwe2lem2  41436  islssfg  41455  unielss  41610  onmaxnelsup  41615  onsupnmax  41620  onsupeqnmax  41639  tfsconcat0i  41738  ntrneineine0lem  42477  ntrneineine1lem  42478  ntrneiel2  42480  extoimad  42559  grumnudlem  42687  supsubc  43708  infxrbnd2  43724  supminfxr  43819  evthiccabs  43854  elicores  43891  clim2f  43997  clim2cf  44011  clim0cf  44015  clim2f2  44031  limsupub  44065  limsupmnflem  44081  limsupre2lem  44085  limsuplt2  44114  liminfreuzlem  44163  liminfltlem  44165  liminflimsupclim  44168  xlimmnfmpt  44204  xlimpnfmpt  44205  fourierdlem73  44540  fourierdlem83  44550  meaiuninc3v  44845  ovolval2  45005  cfsetsnfsetfo  45414  dfaimafn  45517  iccelpart  45745  sprsymrelf  45807  sprsymrelfo  45809  fmtnoprmfac1  45877  fmtnoprmfac2  45879  fmtnofac2lem  45880  dfeven2  45961  dfodd3  45962  isomuspgrlem2d  46143  uspgrsprfo  46170  elbigo2  46758  rrxlinesc  46941  rrxlinec  46942  rrx2line  46946  rrx2vlinest  46947  itsclquadeu  46983