Theorem rexbidva 3174

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-rex 3068

This theorem is referenced by:  rexbidv  3176  2rexbiia  3215  2rexbidva  3217  rexeqbidva  3330  frinxp  5770  onfr  6424  dfimafn  6970  funimass4  6972  fliftel  7328  fliftf  7334  isomin  7356  f1oiso  7370  releldm2  8066  oaass  8597  eldifsucnn  8700  cofonr  8710  naddunif  8729  qsinxp  8831  qliftel  8838  fimaxg  9320  ordunifi  9323  supisolem  9510  fiming  9535  wemapwe  9734  ttrcltr  9753  ttrclse  9764  frmin  9786  cflim2  10300  cfsmolem  10307  alephsing  10313  brdom7disj  10568  brdom6disj  10569  alephreg  10619  nqereu  10966  1idpr  11066  map2psrpr  11147  axsup  11333  rereccl  11982  sup3  12222  infm3  12224  supadd  12233  creur  12257  creui  12258  nndiv  12309  nnrecl  12521  rpnnen1lem2  13016  rpnnen1lem1  13017  rpnnen1lem3  13018  rpnnen1lem5  13020  supxrbnd1  13359  supxrbnd2  13360  supxrbnd  13366  rabssnn0fi  14023  mptnn0fsupp  14034  expnlbnd  14268  wrdl3s3  14997  limsuplt  15511  clim2  15536  clim2c  15537  clim0c  15539  ello12  15548  elo12  15559  rlimresb  15597  climabs0  15617  sumeq2ii  15725  mertens  15918  prodeq2ii  15943  zprod  15969  nndivides  16296  alzdvds  16353  oddm1even  16376  oddnn02np1  16381  oddge22np1  16382  evennn02n  16383  evennn2n  16384  divalglem4  16429  divalgb  16437  modremain  16441  modprmn0modprm0  16840  vdwlem6  17019  vdwlem11  17024  vdw  17027  ramval  17041  imasleval  17587  dfiso3  17820  fullestrcsetc  18206  fullsetcestrc  18221  isipodrs  18594  ipodrsfi  18596  gsumpropd2lem  18704  mndpropd  18784  grppropd  18981  qus0subgbas  19228  conjnmzb  19283  symgextfo  19454  symgfixfo  19471  sylow1lem2  19631  sylow3lem1  19659  sylow3lem3  19661  lsmelvalm  19683  lsmass  19701  iscyg3  19918  ghmcyg  19928  cycsubgcyg  19933  pgpfac1lem2  20109  pgpfac1lem4  20112  ablfac2  20123  dvdsr02  20388  crngunit  20394  dvdsrpropd  20432  rngqiprngimfo  21328  lpigen  21362  pzriprnglem10  21518  znunit  21599  elfilspd  21840  psdmul  22187  scmatmats  22532  symgmatr01  22675  isclo  23110  iscnp3  23267  lmbrf  23283  cncnp  23303  lmss  23321  isnrm2  23381  cmpfi  23431  1stcfb  23468  1stccnp  23485  ptrescn  23662  txkgen  23675  xkoinjcn  23710  trfil3  23911  fmid  23983  lmflf  24028  txflf  24029  ptcmplem3  24077  tsmsf1o  24168  ucnprima  24306  metrest  24552  metcnp  24569  metcnp2  24570  txmetcnp  24575  metuel2  24593  metustbl  24594  psmetutop  24595  metucn  24599  evth2  25005  lmmbrf  25309  iscfil2  25313  fmcfil  25319  iscau2  25324  iscau4  25326  iscauf  25327  caucfil  25330  iscmet3lem3  25337  cfilresi  25342  causs  25345  lmclim  25350  ivth2  25503  ovolfioo  25515  ovolficc  25516  ovolshftlem1  25557  ovolscalem1  25561  volsup2  25653  ismbf3d  25702  mbfaddlem  25708  mbfsup  25712  mbfinf  25713  itg2seq  25791  itg2gt0  25809  ellimc2  25926  ellimc3  25928  rolle  26042  cmvth  26043  cmvthOLD  26044  mvth  26045  dvlip  26046  dvivth  26063  lhop1lem  26066  deg1ldg  26145  ulm2  26442  ulmdvlem3  26459  dcubic  26903  mcubic  26904  cubic2  26905  rlimcnp  27022  ftalem3  27132  isppw2  27172  lgsquadlem2  27439  2lgslem1a  27449  dchrmusumlema  27551  dchrisum0lema  27572  cofcutr  27972  lrrecfr  27990  addsrid  28011  addscom  28013  addsuniflem  28048  addsass  28052  addsbday  28064  negsunif  28101  mulsrid  28153  mulsasslem3  28205  n0s0suc  28359  renegscl  28444  readdscl  28445  remulscllem2  28447  remulscl  28448  tglowdim2l  28672  mirreu3  28676  oppcom  28766  iscgra1  28832  axsegcon  28956  axpasch  28970  axcontlem7  28999  usgr2pth0  29797  usgr2wspthon  29994  elwwlks2  29995  elwspths2spth  29996  rusgrnumwwlks  30003  clwwlkfo  30078  eclclwwlkn1  30103  eucrctshift  30271  fusgreg2wsp  30364  nmobndi  30803  nmounbi  30804  nmoo0  30819  h2hcau  31007  h2hlm  31008  shsel3  31343  pjhtheu2  31444  chscllem2  31666  adjbdln  32111  branmfn  32133  pjimai  32204  chrelati  32392  cdj3lem3  32466  cdj3lem3b  32468  dfimafnf  32652  ofpreima  32681  isarchi2  33174  submarchi  33175  archirng  33177  archiabl  33187  isarchiofld  33326  ellspds  33375  dvdsruasso2  33393  lsmssass  33409  grplsm0l  33410  fedgmullem2  33657  elirng  33700  zarcls  33834  ordtconnlem1  33884  lmdvg  33913  esumfsup  34050  dya2icoseg2  34259  eulerpartlemgh  34359  ballotlemodife  34478  ballotlemsima  34496  nummin  35083  erdszelem10  35184  iscvm  35243  wsuclem  35806  seglelin  36097  outsideofeu  36112  opnrebl  36302  opnrebl2  36303  filnetlem4  36363  bj-finsumval0  37267  phpreu  37590  ptrest  37605  poimirlem3  37609  poimirlem4  37610  poimirlem17  37623  poimirlem26  37632  poimirlem27  37633  broucube  37640  mblfinlem1  37643  lmclim2  37744  caures  37746  isbnd3b  37771  heiborlem7  37803  heiborlem10  37806  rrncmslem  37818  isdrngo2  37944  erimeq2  38659  prter3  38863  islshpsm  38961  lsatfixedN  38990  lrelat  38995  eqlkr2  39081  lshpkrlem1  39091  lfl1dim  39102  eqlkr4  39146  ishlat3N  39335  hlsupr2  39369  hlrelat5N  39383  hlrelat  39384  cvrval5  39397  cvrat42  39426  athgt  39438  3dim0  39439  islln3  39492  llnexatN  39503  islpln3  39515  islvol3  39558  islvol5  39561  isline4N  39759  polval2N  39888  4atex3  40063  cdleme0ex2N  40206  cdlemefrs29cpre1  40380  cdlemb3  40588  cdlemg33c  40690  cdlemg33e  40692  dia1dim2  41044  cdlemm10N  41100  dib1dim2  41150  diclspsn  41176  dih1dimatlem  41311  dihatexv2  41321  djhcvat42  41397  dihjat1lem  41410  dvh4dimat  41420  dvh2dimatN  41422  lcfrlem9  41532  mapdval4N  41614  mapdcv  41642  ef11d  42353  cxp112d  42355  cxp111d  42356  sn-sup3d  42478  fimgmcyc  42520  infdesc  42629  elrfirn  42682  elrfirn2  42683  mrefg3  42695  diophin  42759  diophun  42760  diophren  42800  rmxycomplete  42905  wepwsolem  43030  fnwe2lem2  43039  islssfg  43058  unielss  43206  onmaxnelsup  43211  onsupnmax  43216  onsupeqnmax  43235  tfsconcat0i  43334  ntrneineine0lem  44072  ntrneineine1lem  44073  ntrneiel2  44075  extoimad  44153  grumnudlem  44280  supsubc  45302  infxrbnd2  45318  supminfxr  45413  evthiccabs  45448  elicores  45485  clim2f  45591  clim2cf  45605  clim0cf  45609  clim2f2  45625  limsupub  45659  limsupmnflem  45675  limsupre2lem  45679  limsuplt2  45708  liminfreuzlem  45757  liminfltlem  45759  liminflimsupclim  45762  xlimmnfmpt  45798  xlimpnfmpt  45799  fourierdlem73  46134  fourierdlem83  46144  meaiuninc3v  46439  ovolval2  46599  cfsetsnfsetfo  47009  dfaimafn  47114  iccelpart  47357  sprsymrelf  47419  sprsymrelfo  47421  fmtnoprmfac1  47489  fmtnoprmfac2  47491  fmtnofac2lem  47492  dfeven2  47573  dfodd3  47574  dfvopnbgr2  47776  usgrgrtrirex  47852  stgredgiun  47860  uspgrsprfo  47991  elbigo2  48401  rrxlinesc  48584  rrxlinec  48585  rrx2line  48589  rrx2vlinest  48590  itsclquadeu  48626