Theorem rexbidva 3184

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3087

This theorem is used by:  rexbidv  3186  2rexbiia  3223  2rexbidva  3225  rexeqbidva  3326  frinxp  5738  onfr  6397  dfimafn  6940  funimass4  6942  fliftel  7310  fliftf  7316  isomin  7338  f1oiso  7352  releldm2  8040  oaass  8548  eldifsucnn  8652  cofonr  8662  naddunif  8682  qsinxp  8793  qliftel  8800  fimaxg  9257  ordunifi  9260  supisolem  9444  fiming  9470  wemapwe  9676  ttrcltr  9695  ttrclse  9706  frmin  9731  cflim2  10265  cfsmolem  10272  alephsing  10278  brdom7disj  10534  brdom6disj  10535  alephreg  10591  nqereu  10938  1idpr  11038  map2psrpr  11119  axsup  11309  rereccl  11957  sup3  12196  infm3  12198  supadd  12207  creur  12236  creui  12237  nndiv  12306  nnrecl  12526  rpnnen1lem2  13027  rpnnen1lem1  13028  rpnnen1lem3  13029  rpnnen1lem5  13031  supxrbnd1  13373  supxrbnd2  13374  supxrbnd  13380  rabssnn0fi  14050  mptnn0fsupp  14061  expnlbnd  14297  wrdl3s3  15035  limsuplt  15566  clim2  15591  clim2c  15592  clim0c  15594  ello12  15603  elo12  15614  rlimresb  15652  climabs0  15672  sumeq2ii  15780  mertens  15975  prodeq2ii  16000  zprod  16024  nndivides  16352  alzdvds  16410  oddm1even  16433  oddnn02np1  16438  oddge22np1  16439  evennn02n  16440  evennn2n  16441  divalglem4  16486  divalgb  16494  modremain  16498  modprmn0modprm0  16899  vdwlem6  17078  vdwlem11  17083  vdw  17086  ramval  17100  imasleval  17627  dfiso3  17862  fullestrcsetc  18239  fullsetcestrc  18254  isipodrs  18625  ipodrsfi  18627  mgmidpfod  18770  gsumpropd2lem  18781  mndpropd  18864  grppropd  19075  qus0subgbas  19326  conjnmzb  19380  symgextfo  19549  symgfixfo  19566  sylow1lem2  19726  sylow3lem1  19754  sylow3lem3  19756  lsmelvalm  19778  lsmass  19796  iscyg3  20013  ghmcyg  20023  cycsubgcyg  20028  pgpfac1lem2  20204  pgpfac1lem4  20207  ablfac2  20218  dvdsr02  20513  crngunit  20519  dvdsrpropd  20557  rngqiprngimfo  21504  lpigen  21566  pzriprnglem10  21703  znunit  21776  elfilspd  22016  psdmul  22394  scmatmats  22733  symgmatr01  22876  isclo  23312  iscnp3  23469  lmbrf  23485  cncnp  23505  lmss  23523  isnrm2  23583  cmpfi  23633  1stcfb  23670  1stccnp  23688  ptrescn  23865  txkgen  23878  xkoinjcn  23913  trfil3  24114  fmid  24186  lmflf  24231  txflf  24232  ptcmplem3  24280  tsmsf1o  24371  ucnprima  24507  metrest  24750  metcnp  24767  metcnp2  24768  txmetcnp  24773  metuel2  24791  metustbl  24792  psmetutop  24793  metucn  24797  evth2  25188  lmmbrf  25490  iscfil2  25494  fmcfil  25500  iscau2  25505  iscau4  25507  iscauf  25508  caucfil  25511  iscmet3lem3  25518  cfilresi  25523  causs  25526  lmclim  25531  ivth2  25683  ovolfioo  25695  ovolficc  25696  ovolshftlem1  25737  ovolscalem1  25741  volsup2  25833  ismbf3d  25882  mbfaddlem  25888  mbfsup  25892  mbfinf  25893  itg2seq  25970  itg2gt0  25988  ellimc2  26104  ellimc3  26106  rolle  26217  cmvth  26218  mvth  26219  dvlip  26220  dvivth  26237  lhop1lem  26240  deg1ldg  26317  rnplynfin  26539  plyconz  26540  ulm2  26621  ulmdvlem3  26638  dcubic  27083  mcubic  27084  cubic2  27085  rlimcnp  27202  ftalem3  27311  isppw2  27351  lgsquadlem2  27617  2lgslem1a  27627  dchrmusumlema  27729  dchrisum0lema  27750  cofcutr  28189  lrrecfr  28208  addsrid  28229  addscom  28231  addsuniflem  28266  addsass  28270  addbday  28283  negsunif  28320  mulsrid  28378  mulsasslem3  28430  n0s0suc  28607  z12sge0  28748  elreno2  28760  renegscl  28763  readdscl  28764  remulscllem2  28766  remulscl  28767  tglowdim2l  28998  mirreu3  29005  oppcom  29099  iscgra1  29196  axsegcon  29384  axpasch  29398  axcontlem7  29427  usgr2pth0  30230  usgr2wspthon  30436  elwwlks2  30437  elwspths2spth  30438  rusgrnumwwlks  30445  clwwlkfo  30520  eclclwwlkn1  30545  eucrctshift  30723  fusgreg2wsp  30816  nmobndi  31256  nmounbi  31257  nmoo0  31272  h2hcau  31460  h2hlm  31461  shsel3  31796  pjhtheu2  31897  chscllem2  32119  adjbdln  32564  branmfn  32586  pjimai  32657  chrelati  32845  cdj3lem3  32919  cdj3lem3b  32921  dfimafnf  33109  ofpreima  33138  isarchi2  33625  submarchi  33626  archirng  33628  archiabl  33638  isarchiofld  33639  isunitc  33681  ellspds  33803  dvdsruasso2  33819  lsmssass  33831  grplsm0l  33832  fedgmullem2  34140  elirng  34196  zarcls  34384  ordtconnlem1  34434  lmdvg  34463  esumfsup  34580  dya2icoseg2  34789  eulerpartlemgh  34889  ballotlemodife  35009  ballotlemsima  35027  nummin  35598  erdszelem10  35779  iscvm  35838  wsuclem  36402  seglelin  36696  outsideofeu  36711  ltnadd  36798  naddle  36799  opnrebl  36939  opnrebl2  36940  filnetlem4  37000  bj-finsumval0  38037  phpreu  38358  ptrest  38368  poimirlem3  38372  poimirlem4  38373  poimirlem17  38386  poimirlem26  38395  poimirlem27  38396  broucube  38403  mblfinlem1  38406  lmclim2  38508  caures  38510  isbnd3b  38535  heiborlem7  38567  heiborlem10  38570  rrncmslem  38582  isdrngo2  38708  erimeq2  39511  prter3  39755  islshpsm  39853  lsatfixedN  39882  lrelat  39887  eqlkr2  39973  lshpkrlem1  39983  lfl1dim  39994  eqlkr4  40038  ishlat3N  40227  hlsupr2  40260  hlrelat5N  40274  hlrelat  40275  cvrval5  40288  cvrat42  40317  athgt  40329  3dim0  40330  islln3  40383  llnexatN  40394  islpln3  40406  islvol3  40449  islvol5  40452  isline4N  40650  polval2N  40779  4atex3  40954  cdleme0ex2N  41097  cdlemefrs29cpre1  41271  cdlemb3  41479  cdlemg33c  41581  cdlemg33e  41583  dia1dim2  41935  cdlemm10N  41991  dib1dim2  42041  diclspsn  42067  dih1dimatlem  42202  dihatexv2  42212  djhcvat42  42288  dihjat1lem  42301  dvh4dimat  42311  dvh2dimatN  42313  lcfrlem9  42423  mapdval4N  42505  mapdcv  42533  ef11d  43214  cxp112d  43216  cxp111d  43217  sn-sup3d  43380  fimgmcyc  43416  infdesc  43489  elrfirn  43540  elrfirn2  43541  mrefg3  43553  diophin  43617  diophun  43618  diophren  43654  rmxycomplete  43758  wepwsolem  43883  fnwe2lem2  43892  islssfg  43911  unielss  44059  onmaxnelsup  44064  onsupnmax  44069  onsupeqnmax  44088  tfsconcat0i  44186  ntrneineine0lem  44923  ntrneineine1lem  44924  ntrneiel2  44926  extoimad  45004  grumnudlem  45109  modelac8prim  45815  supsubc  46183  infxrbnd2  46198  supminfxr  46292  evthiccabs  46326  elicores  46363  clim2f  46464  clim2cf  46478  clim0cf  46482  clim2f2  46498  limsupub  46532  limsupmnflem  46548  limsupre2lem  46552  limsuplt2  46581  liminfreuzlem  46630  liminfltlem  46632  liminflimsupclim  46635  xlimmnfmpt  46671  xlimpnfmpt  46672  fourierdlem73  47007  fourierdlem83  47017  meaiuninc3v  47312  ovolval2  47472  cfsetsnfsetfo  47948  dfaimafn  48053  iccelpart  48333  sprsymrelf  48395  sprsymrelfo  48397  nprmmul1  48427  nprmmul3  48429  fmtnoprmfac1  48468  fmtnoprmfac2  48470  fmtnofac2lem  48471  dfeven2  48565  dfodd3  48566  dfvopnbgr2  48769  usgrgrtrirex  48866  stgredgiun  48874  uspgrsprfo  49064  elbigo2  49482  rrxlinesc  49665  rrxlinec  49666  rrx2line  49670  rrx2vlinest  49671  itsclquadeu  49707