Theorem rexbidva 3154

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3057

This theorem is referenced by:  rexbidv  3156  2rexbiia  3193  2rexbidva  3195  rexeqbidva  3299  frinxp  5697  onfr  6345  dfimafn  6884  funimass4  6886  fliftel  7243  fliftf  7249  isomin  7271  f1oiso  7285  releldm2  7975  oaass  8476  eldifsucnn  8579  cofonr  8589  naddunif  8608  qsinxp  8717  qliftel  8724  fimaxg  9171  ordunifi  9174  supisolem  9358  fiming  9384  wemapwe  9587  ttrcltr  9606  ttrclse  9617  frmin  9642  cflim2  10154  cfsmolem  10161  alephsing  10167  brdom7disj  10422  brdom6disj  10423  alephreg  10473  nqereu  10820  1idpr  10920  map2psrpr  11001  axsup  11188  rereccl  11839  sup3  12079  infm3  12081  supadd  12090  creur  12119  creui  12120  nndiv  12171  nnrecl  12379  rpnnen1lem2  12875  rpnnen1lem1  12876  rpnnen1lem3  12877  rpnnen1lem5  12879  supxrbnd1  13220  supxrbnd2  13221  supxrbnd  13227  rabssnn0fi  13893  mptnn0fsupp  13904  expnlbnd  14140  wrdl3s3  14869  limsuplt  15386  clim2  15411  clim2c  15412  clim0c  15414  ello12  15423  elo12  15434  rlimresb  15472  climabs0  15492  sumeq2ii  15600  mertens  15793  prodeq2ii  15818  zprod  15844  nndivides  16173  alzdvds  16231  oddm1even  16254  oddnn02np1  16259  oddge22np1  16260  evennn02n  16261  evennn2n  16262  divalglem4  16307  divalgb  16315  modremain  16319  modprmn0modprm0  16719  vdwlem6  16898  vdwlem11  16903  vdw  16906  ramval  16920  imasleval  17445  dfiso3  17680  fullestrcsetc  18057  fullsetcestrc  18072  isipodrs  18443  ipodrsfi  18445  gsumpropd2lem  18587  mndpropd  18667  grppropd  18864  qus0subgbas  19110  conjnmzb  19165  symgextfo  19334  symgfixfo  19351  sylow1lem2  19511  sylow3lem1  19539  sylow3lem3  19541  lsmelvalm  19563  lsmass  19581  iscyg3  19798  ghmcyg  19808  cycsubgcyg  19813  pgpfac1lem2  19989  pgpfac1lem4  19992  ablfac2  20003  dvdsr02  20290  crngunit  20296  dvdsrpropd  20334  rngqiprngimfo  21238  lpigen  21272  pzriprnglem10  21427  znunit  21500  elfilspd  21740  psdmul  22081  scmatmats  22426  symgmatr01  22569  isclo  23002  iscnp3  23159  lmbrf  23175  cncnp  23195  lmss  23213  isnrm2  23273  cmpfi  23323  1stcfb  23360  1stccnp  23377  ptrescn  23554  txkgen  23567  xkoinjcn  23602  trfil3  23803  fmid  23875  lmflf  23920  txflf  23921  ptcmplem3  23969  tsmsf1o  24060  ucnprima  24196  metrest  24439  metcnp  24456  metcnp2  24457  txmetcnp  24462  metuel2  24480  metustbl  24481  psmetutop  24482  metucn  24486  evth2  24886  lmmbrf  25189  iscfil2  25193  fmcfil  25199  iscau2  25204  iscau4  25206  iscauf  25207  caucfil  25210  iscmet3lem3  25217  cfilresi  25222  causs  25225  lmclim  25230  ivth2  25383  ovolfioo  25395  ovolficc  25396  ovolshftlem1  25437  ovolscalem1  25441  volsup2  25533  ismbf3d  25582  mbfaddlem  25588  mbfsup  25592  mbfinf  25593  itg2seq  25670  itg2gt0  25688  ellimc2  25805  ellimc3  25807  rolle  25921  cmvth  25922  cmvthOLD  25923  mvth  25924  dvlip  25925  dvivth  25942  lhop1lem  25945  deg1ldg  26024  ulm2  26321  ulmdvlem3  26338  dcubic  26783  mcubic  26784  cubic2  26785  rlimcnp  26902  ftalem3  27012  isppw2  27052  lgsquadlem2  27319  2lgslem1a  27329  dchrmusumlema  27431  dchrisum0lema  27452  cofcutr  27868  lrrecfr  27886  addsrid  27907  addscom  27909  addsuniflem  27944  addsass  27948  addsbday  27960  negsunif  27997  mulsrid  28052  mulsasslem3  28104  n0s0suc  28270  zs12ge0  28393  renegscl  28400  readdscl  28401  remulscllem2  28403  remulscl  28404  tglowdim2l  28628  mirreu3  28632  oppcom  28722  iscgra1  28788  axsegcon  28905  axpasch  28919  axcontlem7  28948  usgr2pth0  29743  usgr2wspthon  29946  elwwlks2  29947  elwspths2spth  29948  rusgrnumwwlks  29955  clwwlkfo  30030  eclclwwlkn1  30055  eucrctshift  30223  fusgreg2wsp  30316  nmobndi  30755  nmounbi  30756  nmoo0  30771  h2hcau  30959  h2hlm  30960  shsel3  31295  pjhtheu2  31396  chscllem2  31618  adjbdln  32063  branmfn  32085  pjimai  32156  chrelati  32344  cdj3lem3  32418  cdj3lem3b  32420  dfimafnf  32618  ofpreima  32647  isarchi2  33154  submarchi  33155  archirng  33157  archiabl  33167  isarchiofld  33168  ellspds  33333  dvdsruasso2  33351  lsmssass  33367  grplsm0l  33368  fedgmullem2  33643  elirng  33699  zarcls  33887  ordtconnlem1  33937  lmdvg  33966  esumfsup  34083  dya2icoseg2  34291  eulerpartlemgh  34391  ballotlemodife  34511  ballotlemsima  34529  nummin  35104  erdszelem10  35244  iscvm  35303  wsuclem  35867  seglelin  36160  outsideofeu  36175  opnrebl  36364  opnrebl2  36365  filnetlem4  36425  bj-finsumval0  37329  phpreu  37654  ptrest  37669  poimirlem3  37673  poimirlem4  37674  poimirlem17  37687  poimirlem26  37696  poimirlem27  37697  broucube  37704  mblfinlem1  37707  lmclim2  37808  caures  37810  isbnd3b  37835  heiborlem7  37867  heiborlem10  37870  rrncmslem  37882  isdrngo2  38008  erimeq2  38786  prter3  38991  islshpsm  39089  lsatfixedN  39118  lrelat  39123  eqlkr2  39209  lshpkrlem1  39219  lfl1dim  39230  eqlkr4  39274  ishlat3N  39463  hlsupr2  39496  hlrelat5N  39510  hlrelat  39511  cvrval5  39524  cvrat42  39553  athgt  39565  3dim0  39566  islln3  39619  llnexatN  39630  islpln3  39642  islvol3  39685  islvol5  39688  isline4N  39886  polval2N  40015  4atex3  40190  cdleme0ex2N  40333  cdlemefrs29cpre1  40507  cdlemb3  40715  cdlemg33c  40817  cdlemg33e  40819  dia1dim2  41171  cdlemm10N  41227  dib1dim2  41277  diclspsn  41303  dih1dimatlem  41438  dihatexv2  41448  djhcvat42  41524  dihjat1lem  41537  dvh4dimat  41547  dvh2dimatN  41549  lcfrlem9  41659  mapdval4N  41741  mapdcv  41769  ef11d  42442  cxp112d  42444  cxp111d  42445  sn-sup3d  42595  fimgmcyc  42637  infdesc  42746  elrfirn  42798  elrfirn2  42799  mrefg3  42811  diophin  42875  diophun  42876  diophren  42916  rmxycomplete  43020  wepwsolem  43145  fnwe2lem2  43154  islssfg  43173  unielss  43321  onmaxnelsup  43326  onsupnmax  43331  onsupeqnmax  43350  tfsconcat0i  43448  ntrneineine0lem  44186  ntrneineine1lem  44187  ntrneiel2  44189  extoimad  44267  grumnudlem  44388  modelac8prim  45095  supsubc  45462  infxrbnd2  45477  supminfxr  45572  evthiccabs  45606  elicores  45643  clim2f  45744  clim2cf  45758  clim0cf  45762  clim2f2  45778  limsupub  45812  limsupmnflem  45828  limsupre2lem  45832  limsuplt2  45861  liminfreuzlem  45910  liminfltlem  45912  liminflimsupclim  45915  xlimmnfmpt  45951  xlimpnfmpt  45952  fourierdlem73  46287  fourierdlem83  46297  meaiuninc3v  46592  ovolval2  46752  cfsetsnfsetfo  47170  dfaimafn  47275  iccelpart  47543  sprsymrelf  47605  sprsymrelfo  47607  fmtnoprmfac1  47675  fmtnoprmfac2  47677  fmtnofac2lem  47678  dfeven2  47759  dfodd3  47760  dfvopnbgr2  47963  usgrgrtrirex  48060  stgredgiun  48068  uspgrsprfo  48258  elbigo2  48663  rrxlinesc  48846  rrxlinec  48847  rrx2line  48851  rrx2vlinest  48852  itsclquadeu  48888