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  36158  outsideofeu  36173  opnrebl  36362  opnrebl2  36363  filnetlem4  36423  bj-finsumval0  37327  phpreu  37652  ptrest  37667  poimirlem3  37671  poimirlem4  37672  poimirlem17  37685  poimirlem26  37694  poimirlem27  37695  broucube  37702  mblfinlem1  37705  lmclim2  37806  caures  37808  isbnd3b  37833  heiborlem7  37865  heiborlem10  37868  rrncmslem  37880  isdrngo2  38006  erimeq2  38724  prter3  38929  islshpsm  39027  lsatfixedN  39056  lrelat  39061  eqlkr2  39147  lshpkrlem1  39157  lfl1dim  39168  eqlkr4  39212  ishlat3N  39401  hlsupr2  39434  hlrelat5N  39448  hlrelat  39449  cvrval5  39462  cvrat42  39491  athgt  39503  3dim0  39504  islln3  39557  llnexatN  39568  islpln3  39580  islvol3  39623  islvol5  39626  isline4N  39824  polval2N  39953  4atex3  40128  cdleme0ex2N  40271  cdlemefrs29cpre1  40445  cdlemb3  40653  cdlemg33c  40755  cdlemg33e  40757  dia1dim2  41109  cdlemm10N  41165  dib1dim2  41215  diclspsn  41241  dih1dimatlem  41376  dihatexv2  41386  djhcvat42  41462  dihjat1lem  41475  dvh4dimat  41485  dvh2dimatN  41487  lcfrlem9  41597  mapdval4N  41679  mapdcv  41707  ef11d  42380  cxp112d  42382  cxp111d  42383  sn-sup3d  42533  fimgmcyc  42575  infdesc  42684  elrfirn  42736  elrfirn2  42737  mrefg3  42749  diophin  42813  diophun  42814  diophren  42854  rmxycomplete  42958  wepwsolem  43083  fnwe2lem2  43092  islssfg  43111  unielss  43259  onmaxnelsup  43264  onsupnmax  43269  onsupeqnmax  43288  tfsconcat0i  43386  ntrneineine0lem  44124  ntrneineine1lem  44125  ntrneiel2  44127  extoimad  44205  grumnudlem  44326  modelac8prim  45033  supsubc  45400  infxrbnd2  45415  supminfxr  45510  evthiccabs  45544  elicores  45581  clim2f  45682  clim2cf  45696  clim0cf  45700  clim2f2  45716  limsupub  45750  limsupmnflem  45766  limsupre2lem  45770  limsuplt2  45799  liminfreuzlem  45848  liminfltlem  45850  liminflimsupclim  45853  xlimmnfmpt  45889  xlimpnfmpt  45890  fourierdlem73  46225  fourierdlem83  46235  meaiuninc3v  46530  ovolval2  46690  cfsetsnfsetfo  47099  dfaimafn  47204  iccelpart  47472  sprsymrelf  47534  sprsymrelfo  47536  fmtnoprmfac1  47604  fmtnoprmfac2  47606  fmtnofac2lem  47607  dfeven2  47688  dfodd3  47689  dfvopnbgr2  47892  usgrgrtrirex  47989  stgredgiun  47997  uspgrsprfo  48187  elbigo2  48592  rrxlinesc  48775  rrxlinec  48776  rrx2line  48780  rrx2vlinest  48781  itsclquadeu  48817