Theorem rexbidva 3159

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

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

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 3062

This theorem is referenced by:  rexbidv  3161  2rexbiia  3198  2rexbidva  3200  rexeqbidva  3302  frinxp  5714  onfr  6362  dfimafn  6902  funimass4  6904  fliftel  7264  fliftf  7270  isomin  7292  f1oiso  7306  releldm2  7996  oaass  8496  eldifsucnn  8600  cofonr  8610  naddunif  8629  qsinxp  8740  qliftel  8747  fimaxg  9197  ordunifi  9200  supisolem  9387  fiming  9413  wemapwe  9618  ttrcltr  9637  ttrclse  9648  frmin  9673  cflim2  10185  cfsmolem  10192  alephsing  10198  brdom7disj  10453  brdom6disj  10454  alephreg  10505  nqereu  10852  1idpr  10952  map2psrpr  11033  axsup  11221  rereccl  11873  sup3  12113  infm3  12115  supadd  12124  creur  12153  creui  12154  nndiv  12223  nnrecl  12435  rpnnen1lem2  12927  rpnnen1lem1  12928  rpnnen1lem3  12929  rpnnen1lem5  12931  supxrbnd1  13273  supxrbnd2  13274  supxrbnd  13280  rabssnn0fi  13948  mptnn0fsupp  13959  expnlbnd  14195  wrdl3s3  14924  limsuplt  15441  clim2  15466  clim2c  15467  clim0c  15469  ello12  15478  elo12  15489  rlimresb  15527  climabs0  15547  sumeq2ii  15655  mertens  15851  prodeq2ii  15876  zprod  15902  nndivides  16231  alzdvds  16289  oddm1even  16312  oddnn02np1  16317  oddge22np1  16318  evennn02n  16319  evennn2n  16320  divalglem4  16365  divalgb  16373  modremain  16377  modprmn0modprm0  16778  vdwlem6  16957  vdwlem11  16962  vdw  16965  ramval  16979  imasleval  17505  dfiso3  17740  fullestrcsetc  18117  fullsetcestrc  18132  isipodrs  18503  ipodrsfi  18505  gsumpropd2lem  18647  mndpropd  18727  grppropd  18927  qus0subgbas  19173  conjnmzb  19228  symgextfo  19397  symgfixfo  19414  sylow1lem2  19574  sylow3lem1  19602  sylow3lem3  19604  lsmelvalm  19626  lsmass  19644  iscyg3  19861  ghmcyg  19871  cycsubgcyg  19876  pgpfac1lem2  20052  pgpfac1lem4  20055  ablfac2  20066  dvdsr02  20352  crngunit  20358  dvdsrpropd  20396  rngqiprngimfo  21299  lpigen  21333  pzriprnglem10  21470  znunit  21543  elfilspd  21783  psdmul  22132  scmatmats  22476  symgmatr01  22619  isclo  23052  iscnp3  23209  lmbrf  23225  cncnp  23245  lmss  23263  isnrm2  23323  cmpfi  23373  1stcfb  23410  1stccnp  23427  ptrescn  23604  txkgen  23617  xkoinjcn  23652  trfil3  23853  fmid  23925  lmflf  23970  txflf  23971  ptcmplem3  24019  tsmsf1o  24110  ucnprima  24246  metrest  24489  metcnp  24506  metcnp2  24507  txmetcnp  24512  metuel2  24530  metustbl  24531  psmetutop  24532  metucn  24536  evth2  24927  lmmbrf  25229  iscfil2  25233  fmcfil  25239  iscau2  25244  iscau4  25246  iscauf  25247  caucfil  25250  iscmet3lem3  25257  cfilresi  25262  causs  25265  lmclim  25270  ivth2  25422  ovolfioo  25434  ovolficc  25435  ovolshftlem1  25476  ovolscalem1  25480  volsup2  25572  ismbf3d  25621  mbfaddlem  25627  mbfsup  25631  mbfinf  25632  itg2seq  25709  itg2gt0  25727  ellimc2  25844  ellimc3  25846  rolle  25957  cmvth  25958  mvth  25959  dvlip  25960  dvivth  25977  lhop1lem  25980  deg1ldg  26057  ulm2  26350  ulmdvlem3  26367  dcubic  26810  mcubic  26811  cubic2  26812  rlimcnp  26929  ftalem3  27038  isppw2  27078  lgsquadlem2  27344  2lgslem1a  27354  dchrmusumlema  27456  dchrisum0lema  27477  cofcutr  27916  lrrecfr  27935  addsrid  27956  addscom  27958  addsuniflem  27993  addsass  27997  addbday  28010  negsunif  28047  mulsrid  28105  mulsasslem3  28157  n0s0suc  28334  z12sge0  28475  elreno2  28487  renegscl  28490  readdscl  28491  remulscllem2  28493  remulscl  28494  tglowdim2l  28718  mirreu3  28722  oppcom  28812  iscgra1  28878  axsegcon  28996  axpasch  29010  axcontlem7  29039  usgr2pth0  29833  usgr2wspthon  30036  elwwlks2  30037  elwspths2spth  30038  rusgrnumwwlks  30045  clwwlkfo  30120  eclclwwlkn1  30145  eucrctshift  30313  fusgreg2wsp  30406  nmobndi  30846  nmounbi  30847  nmoo0  30862  h2hcau  31050  h2hlm  31051  shsel3  31386  pjhtheu2  31487  chscllem2  31709  adjbdln  32154  branmfn  32176  pjimai  32247  chrelati  32435  cdj3lem3  32509  cdj3lem3b  32511  dfimafnf  32709  ofpreima  32738  isarchi2  33246  submarchi  33247  archirng  33249  archiabl  33259  isarchiofld  33260  ellspds  33428  dvdsruasso2  33446  lsmssass  33462  grplsm0l  33463  fedgmullem2  33774  elirng  33830  zarcls  34018  ordtconnlem1  34068  lmdvg  34097  esumfsup  34214  dya2icoseg2  34422  eulerpartlemgh  34522  ballotlemodife  34642  ballotlemsima  34660  nummin  35236  erdszelem10  35382  iscvm  35441  wsuclem  36005  seglelin  36298  outsideofeu  36313  opnrebl  36502  opnrebl2  36503  filnetlem4  36563  bj-finsumval0  37599  phpreu  37925  ptrest  37940  poimirlem3  37944  poimirlem4  37945  poimirlem17  37958  poimirlem26  37967  poimirlem27  37968  broucube  37975  mblfinlem1  37978  lmclim2  38079  caures  38081  isbnd3b  38106  heiborlem7  38138  heiborlem10  38141  rrncmslem  38153  isdrngo2  38279  erimeq2  39084  prter3  39328  islshpsm  39426  lsatfixedN  39455  lrelat  39460  eqlkr2  39546  lshpkrlem1  39556  lfl1dim  39567  eqlkr4  39611  ishlat3N  39800  hlsupr2  39833  hlrelat5N  39847  hlrelat  39848  cvrval5  39861  cvrat42  39890  athgt  39902  3dim0  39903  islln3  39956  llnexatN  39967  islpln3  39979  islvol3  40022  islvol5  40025  isline4N  40223  polval2N  40352  4atex3  40527  cdleme0ex2N  40670  cdlemefrs29cpre1  40844  cdlemb3  41052  cdlemg33c  41154  cdlemg33e  41156  dia1dim2  41508  cdlemm10N  41564  dib1dim2  41614  diclspsn  41640  dih1dimatlem  41775  dihatexv2  41785  djhcvat42  41861  dihjat1lem  41874  dvh4dimat  41884  dvh2dimatN  41886  lcfrlem9  41996  mapdval4N  42078  mapdcv  42106  ef11d  42771  cxp112d  42773  cxp111d  42774  sn-sup3d  42937  fimgmcyc  42979  infdesc  43076  elrfirn  43127  elrfirn2  43128  mrefg3  43140  diophin  43204  diophun  43205  diophren  43241  rmxycomplete  43345  wepwsolem  43470  fnwe2lem2  43479  islssfg  43498  unielss  43646  onmaxnelsup  43651  onsupnmax  43656  onsupeqnmax  43675  tfsconcat0i  43773  ntrneineine0lem  44510  ntrneineine1lem  44511  ntrneiel2  44513  extoimad  44591  grumnudlem  44712  modelac8prim  45419  supsubc  45783  infxrbnd2  45798  supminfxr  45892  evthiccabs  45926  elicores  45963  clim2f  46064  clim2cf  46078  clim0cf  46082  clim2f2  46098  limsupub  46132  limsupmnflem  46148  limsupre2lem  46152  limsuplt2  46181  liminfreuzlem  46230  liminfltlem  46232  liminflimsupclim  46235  xlimmnfmpt  46271  xlimpnfmpt  46272  fourierdlem73  46607  fourierdlem83  46617  meaiuninc3v  46912  ovolval2  47072  cfsetsnfsetfo  47508  dfaimafn  47613  iccelpart  47893  sprsymrelf  47955  sprsymrelfo  47957  nprmmul1  47987  nprmmul3  47989  fmtnoprmfac1  48028  fmtnoprmfac2  48030  fmtnofac2lem  48031  dfeven2  48125  dfodd3  48126  dfvopnbgr2  48329  usgrgrtrirex  48426  stgredgiun  48434  uspgrsprfo  48624  elbigo2  49028  rrxlinesc  49211  rrxlinec  49212  rrx2line  49216  rrx2vlinest  49217  itsclquadeu  49253