Theorem rexbidva 3155

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  rexbidv  3157  2rexbiia  3196  2rexbidva  3198  rexeqbidva  3303  frinxp  5714  onfr  6359  dfimafn  6905  funimass4  6907  fliftel  7266  fliftf  7272  isomin  7294  f1oiso  7308  releldm2  8001  oaass  8502  eldifsucnn  8605  cofonr  8615  naddunif  8634  qsinxp  8743  qliftel  8750  fimaxg  9210  ordunifi  9213  supisolem  9401  fiming  9427  wemapwe  9626  ttrcltr  9645  ttrclse  9656  frmin  9678  cflim2  10192  cfsmolem  10199  alephsing  10205  brdom7disj  10460  brdom6disj  10461  alephreg  10511  nqereu  10858  1idpr  10958  map2psrpr  11039  axsup  11225  rereccl  11876  sup3  12116  infm3  12118  supadd  12127  creur  12156  creui  12157  nndiv  12208  nnrecl  12416  rpnnen1lem2  12912  rpnnen1lem1  12913  rpnnen1lem3  12914  rpnnen1lem5  12916  supxrbnd1  13257  supxrbnd2  13258  supxrbnd  13264  rabssnn0fi  13927  mptnn0fsupp  13938  expnlbnd  14174  wrdl3s3  14904  limsuplt  15421  clim2  15446  clim2c  15447  clim0c  15449  ello12  15458  elo12  15469  rlimresb  15507  climabs0  15527  sumeq2ii  15635  mertens  15828  prodeq2ii  15853  zprod  15879  nndivides  16208  alzdvds  16266  oddm1even  16289  oddnn02np1  16294  oddge22np1  16295  evennn02n  16296  evennn2n  16297  divalglem4  16342  divalgb  16350  modremain  16354  modprmn0modprm0  16754  vdwlem6  16933  vdwlem11  16938  vdw  16941  ramval  16955  imasleval  17480  dfiso3  17711  fullestrcsetc  18088  fullsetcestrc  18103  isipodrs  18472  ipodrsfi  18474  gsumpropd2lem  18582  mndpropd  18662  grppropd  18859  qus0subgbas  19106  conjnmzb  19161  symgextfo  19328  symgfixfo  19345  sylow1lem2  19505  sylow3lem1  19533  sylow3lem3  19535  lsmelvalm  19557  lsmass  19575  iscyg3  19792  ghmcyg  19802  cycsubgcyg  19807  pgpfac1lem2  19983  pgpfac1lem4  19986  ablfac2  19997  dvdsr02  20257  crngunit  20263  dvdsrpropd  20301  rngqiprngimfo  21187  lpigen  21221  pzriprnglem10  21376  znunit  21449  elfilspd  21688  psdmul  22029  scmatmats  22374  symgmatr01  22517  isclo  22950  iscnp3  23107  lmbrf  23123  cncnp  23143  lmss  23161  isnrm2  23221  cmpfi  23271  1stcfb  23308  1stccnp  23325  ptrescn  23502  txkgen  23515  xkoinjcn  23550  trfil3  23751  fmid  23823  lmflf  23868  txflf  23869  ptcmplem3  23917  tsmsf1o  24008  ucnprima  24145  metrest  24388  metcnp  24405  metcnp2  24406  txmetcnp  24411  metuel2  24429  metustbl  24430  psmetutop  24431  metucn  24435  evth2  24835  lmmbrf  25138  iscfil2  25142  fmcfil  25148  iscau2  25153  iscau4  25155  iscauf  25156  caucfil  25159  iscmet3lem3  25166  cfilresi  25171  causs  25174  lmclim  25179  ivth2  25332  ovolfioo  25344  ovolficc  25345  ovolshftlem1  25386  ovolscalem1  25390  volsup2  25482  ismbf3d  25531  mbfaddlem  25537  mbfsup  25541  mbfinf  25542  itg2seq  25619  itg2gt0  25637  ellimc2  25754  ellimc3  25756  rolle  25870  cmvth  25871  cmvthOLD  25872  mvth  25873  dvlip  25874  dvivth  25891  lhop1lem  25894  deg1ldg  25973  ulm2  26270  ulmdvlem3  26287  dcubic  26732  mcubic  26733  cubic2  26734  rlimcnp  26851  ftalem3  26961  isppw2  27001  lgsquadlem2  27268  2lgslem1a  27278  dchrmusumlema  27380  dchrisum0lema  27401  cofcutr  27808  lrrecfr  27826  addsrid  27847  addscom  27849  addsuniflem  27884  addsass  27888  addsbday  27900  negsunif  27937  mulsrid  27992  mulsasslem3  28044  n0s0suc  28210  zs12ge0  28318  renegscl  28325  readdscl  28326  remulscllem2  28328  remulscl  28329  tglowdim2l  28553  mirreu3  28557  oppcom  28647  iscgra1  28713  axsegcon  28830  axpasch  28844  axcontlem7  28873  usgr2pth0  29668  usgr2wspthon  29868  elwwlks2  29869  elwspths2spth  29870  rusgrnumwwlks  29877  clwwlkfo  29952  eclclwwlkn1  29977  eucrctshift  30145  fusgreg2wsp  30238  nmobndi  30677  nmounbi  30678  nmoo0  30693  h2hcau  30881  h2hlm  30882  shsel3  31217  pjhtheu2  31318  chscllem2  31540  adjbdln  31985  branmfn  32007  pjimai  32078  chrelati  32266  cdj3lem3  32340  cdj3lem3b  32342  dfimafnf  32533  ofpreima  32562  isarchi2  33112  submarchi  33113  archirng  33115  archiabl  33125  isarchiofld  33268  ellspds  33312  dvdsruasso2  33330  lsmssass  33346  grplsm0l  33347  fedgmullem2  33599  elirng  33654  zarcls  33837  ordtconnlem1  33887  lmdvg  33916  esumfsup  34033  dya2icoseg2  34242  eulerpartlemgh  34342  ballotlemodife  34462  ballotlemsima  34480  nummin  35054  erdszelem10  35160  iscvm  35219  wsuclem  35786  seglelin  36077  outsideofeu  36092  opnrebl  36281  opnrebl2  36282  filnetlem4  36342  bj-finsumval0  37246  phpreu  37571  ptrest  37586  poimirlem3  37590  poimirlem4  37591  poimirlem17  37604  poimirlem26  37613  poimirlem27  37614  broucube  37621  mblfinlem1  37624  lmclim2  37725  caures  37727  isbnd3b  37752  heiborlem7  37784  heiborlem10  37787  rrncmslem  37799  isdrngo2  37925  erimeq2  38643  prter3  38848  islshpsm  38946  lsatfixedN  38975  lrelat  38980  eqlkr2  39066  lshpkrlem1  39076  lfl1dim  39087  eqlkr4  39131  ishlat3N  39320  hlsupr2  39354  hlrelat5N  39368  hlrelat  39369  cvrval5  39382  cvrat42  39411  athgt  39423  3dim0  39424  islln3  39477  llnexatN  39488  islpln3  39500  islvol3  39543  islvol5  39546  isline4N  39744  polval2N  39873  4atex3  40048  cdleme0ex2N  40191  cdlemefrs29cpre1  40365  cdlemb3  40573  cdlemg33c  40675  cdlemg33e  40677  dia1dim2  41029  cdlemm10N  41085  dib1dim2  41135  diclspsn  41161  dih1dimatlem  41296  dihatexv2  41306  djhcvat42  41382  dihjat1lem  41395  dvh4dimat  41405  dvh2dimatN  41407  lcfrlem9  41517  mapdval4N  41599  mapdcv  41627  ef11d  42300  cxp112d  42302  cxp111d  42303  sn-sup3d  42453  fimgmcyc  42495  infdesc  42604  elrfirn  42656  elrfirn2  42657  mrefg3  42669  diophin  42733  diophun  42734  diophren  42774  rmxycomplete  42879  wepwsolem  43004  fnwe2lem2  43013  islssfg  43032  unielss  43180  onmaxnelsup  43185  onsupnmax  43190  onsupeqnmax  43209  tfsconcat0i  43307  ntrneineine0lem  44045  ntrneineine1lem  44046  ntrneiel2  44048  extoimad  44126  grumnudlem  44247  modelac8prim  44955  supsubc  45322  infxrbnd2  45338  supminfxr  45433  evthiccabs  45467  elicores  45504  clim2f  45607  clim2cf  45621  clim0cf  45625  clim2f2  45641  limsupub  45675  limsupmnflem  45691  limsupre2lem  45695  limsuplt2  45724  liminfreuzlem  45773  liminfltlem  45775  liminflimsupclim  45778  xlimmnfmpt  45814  xlimpnfmpt  45815  fourierdlem73  46150  fourierdlem83  46160  meaiuninc3v  46455  ovolval2  46615  cfsetsnfsetfo  47034  dfaimafn  47139  iccelpart  47407  sprsymrelf  47469  sprsymrelfo  47471  fmtnoprmfac1  47539  fmtnoprmfac2  47541  fmtnofac2lem  47542  dfeven2  47623  dfodd3  47624  dfvopnbgr2  47826  usgrgrtrirex  47922  stgredgiun  47930  uspgrsprfo  48109  elbigo2  48514  rrxlinesc  48697  rrxlinec  48698  rrx2line  48702  rrx2vlinest  48703  itsclquadeu  48739