Theorem rexbidva 3188

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

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

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 1945

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

This theorem is used by:  rexbidv  3190  2rexbiia  3227  2rexbidva  3229  rexeqbidva  3330  frinxp  5742  onfr  6428  dfimafn  6978  funimass4  6980  fliftel  7348  fliftf  7354  isomin  7376  f1oiso  7390  releldm2  8088  fnwe2lem3  8184  oaass  8607  eldifsucnn  8711  cofonr  8721  naddunif  8741  qsinxp  8852  qliftel  8859  fimaxg  9316  ordunifi  9319  supisolem  9503  fiming  9529  wemapwe  9735  ttrcltr  9754  ttrclse  9765  frmin  9790  cflim2  10380  cfsmolem  10387  alephsing  10393  brdom7disj  10649  brdom6disj  10650  alephreg  10706  nqereu  11053  1idpr  11153  map2psrpr  11234  axsup  11424  rereccl  12075  sup3  12314  infm3  12316  supadd  12325  creur  12354  creui  12355  nndiv  12424  nnrecl  12644  rpnnen1lem2  13145  rpnnen1lem1  13146  rpnnen1lem3  13147  rpnnen1lem5  13149  supxrbnd1  13491  supxrbnd2  13492  supxrbnd  13498  rabssnn0fi  14169  mptnn0fsupp  14180  expnlbnd  14418  wrdl3s3  15158  limsuplt  15690  clim2  15715  clim2c  15716  clim0c  15718  ello12  15727  elo12  15738  rlimresb  15776  climabs0  15796  sumeq2ii  15904  mertens  16099  prodeq2ii  16124  zprod  16148  nndivides  16476  alzdvds  16534  oddm1even  16557  oddnn02np1  16562  oddge22np1  16563  evennn02n  16564  evennn2n  16565  divalglem4  16610  divalgb  16618  modremain  16622  modprmn0modprm0  17029  vdwlem6  17208  vdwlem11  17213  vdw  17216  ramval  17230  imasleval  17763  dfiso3  17998  fullestrcsetc  18375  fullsetcestrc  18390  isipodrs  18761  ipodrsfi  18763  mgmidpfod  18907  gsumpropd2lem  18918  mndpropd  19001  grppropd  19212  qus0subgbas  19463  conjnmzb  19517  symgextfo  19687  symgfixfo  19704  sylow1lem2  19864  sylow3lem1  19892  sylow3lem3  19894  lsmelvalm  19916  lsmass  19934  iscyg3  20151  ghmcyg  20161  cycsubgcyg  20166  pgpfac1lem2  20342  pgpfac1lem4  20345  ablfac2  20356  dvdsr02  20653  crngunit  20659  dvdsrpropd  20697  rngqiprngimfo  21648  lpigen  21710  pzriprnglem10  21851  znunit  21924  elfilspd  22164  psdmul  22542  scmatmats  22881  symgmatr01  23024  isclo  23460  iscnp3  23617  lmbrf  23633  cncnp  23653  lmss  23671  isnrm2  23731  cmpfi  23781  1stcfb  23818  1stccnp  23836  ptrescn  24013  txkgen  24026  xkoinjcn  24061  trfil3  24262  fmid  24334  lmflf  24379  txflf  24380  ptcmplem3  24428  tsmsf1o  24519  ucnprima  24655  metrest  24898  metcnp  24915  metcnp2  24916  txmetcnp  24921  metuel2  24939  metustbl  24940  psmetutop  24941  metucn  24945  evth2  25336  lmmbrf  25638  iscfil2  25642  fmcfil  25648  iscau2  25653  iscau4  25655  iscauf  25656  caucfil  25659  iscmet3lem3  25666  cfilresi  25671  causs  25674  lmclim  25679  ivth2  25831  ovolfioo  25843  ovolficc  25844  ovolshftlem1  25885  ovolscalem1  25889  volsup2  25981  ismbf3d  26030  mbfaddlem  26036  mbfsup  26040  mbfinf  26041  itg2seq  26118  itg2gt0  26136  ellimc2  26252  ellimc3  26254  rolle  26365  cmvth  26366  mvth  26367  dvlip  26368  dvivth  26385  lhop1lem  26388  deg1ldg  26465  rnplynfin  26685  plyconz  26686  ulm2  26769  ulmdvlem3  26786  dcubic  27231  mcubic  27232  cubic2  27233  rlimcnp  27350  ftalem3  27459  isppw2  27499  lgsquadlem2  27765  2lgslem1a  27775  dchrmusumlema  27877  dchrisum0lema  27898  infdesc  28024  cofcutr  28367  lrrecfr  28386  addsrid  28407  addscom  28409  addsuniflem  28444  addsass  28448  addbday  28461  negsunif  28498  mulsrid  28556  mulsasslem3  28608  n0s0suc  28785  z12sge0  28926  elreno2  28938  renegscl  28941  readdscl  28942  remulscllem2  28944  remulscl  28945  tglowdim2l  29176  mirreu3  29183  oppcom  29277  iscgra1  29374  axsegcon  29562  axpasch  29576  axcontlem7  29605  usgr2pth0  30408  usgr2wspthon  30614  elwwlks2  30615  elwspths2spth  30616  rusgrnumwwlks  30623  clwwlkfo  30698  eclclwwlkn1  30723  eucrctshift  30901  fusgreg2wsp  30994  nmobndi  31434  nmounbi  31435  nmoo0  31450  h2hcau  31638  h2hlm  31639  shsel3  31974  pjhtheu2  32075  chscllem2  32297  adjbdln  32742  branmfn  32764  pjimai  32835  chrelati  33023  cdj3lem3  33097  cdj3lem3b  33099  dfimafnf  33328  ofpreima  33357  isarchi2  33845  submarchi  33846  archirng  33848  archiabl  33858  isarchiofld  33859  isunitc  33901  isedom  33953  ellspds  34028  dvdsruasso2  34045  lsmssass  34057  grplsm0l  34058  fedgmullem2  34373  elirng  34429  zarcls  34617  ordtconnlem1  34667  lmdvg  34696  esumfsup  34813  dya2icoseg2  35021  eulerpartlemgh  35121  ballotlemodife  35241  ballotlemsima  35259  nummin  35847  erdszelem10  36173  iscvm  36232  wsuclem  36802  seglelin  37096  outsideofeu  37111  ltnadd  37182  naddle  37183  opnrebl  37323  opnrebl2  37324  filnetlem4  37384  bj-finsumval0  38474  phpreu  38795  ptrest  38805  poimirlem3  38809  poimirlem4  38810  poimirlem17  38823  poimirlem26  38832  poimirlem27  38833  broucube  38840  mblfinlem1  38843  lmclim2  38958  caures  38960  isbnd3b  38985  heiborlem7  39017  heiborlem10  39020  rrncmslem  39032  isdrngo2  39158  erimeq2  39961  prter3  40205  islshpsm  40303  lsatfixedN  40332  lrelat  40337  eqlkr2  40423  lshpkrlem1  40433  lfl1dim  40444  eqlkr4  40488  ishlat3N  40677  hlsupr2  40710  hlrelat5N  40724  hlrelat  40725  cvrval5  40738  cvrat42  40767  athgt  40779  3dim0  40780  islln3  40833  llnexatN  40844  islpln3  40856  islvol3  40899  islvol5  40902  isline4N  41100  polval2N  41229  4atex3  41404  cdleme0ex2N  41547  cdlemefrs29cpre1  41721  cdlemb3  41929  cdlemg33c  42031  cdlemg33e  42033  dia1dim2  42385  cdlemm10N  42441  dib1dim2  42491  diclspsn  42517  dih1dimatlem  42652  dihatexv2  42662  djhcvat42  42738  dihjat1lem  42751  dvh4dimat  42761  dvh2dimatN  42763  lcfrlem9  42873  mapdval4N  42955  mapdcv  42983  ef11d  43656  cxp112d  43658  cxp111d  43659  sn-sup3d  43822  fimgmcyc  43864  elrfirn  43972  elrfirn2  43973  mrefg3  43985  diophin  44049  diophun  44050  diophren  44086  rmxycomplete  44190  wepwsolem  44315  islssfg  44338  unielss  44481  onmaxnelsup  44486  onsupnmax  44491  onsupeqnmax  44510  tfsconcat0i  44608  ntrneineine0lem  45344  ntrneineine1lem  45345  ntrneiel2  45347  extoimad  45425  grumnudlem  45530  modelac8prim  46246  supsubc  46638  infxrbnd2  46653  supminfxr  46747  evthiccabs  46781  elicores  46818  clim2f  46919  clim2cf  46933  clim0cf  46937  clim2f2  46953  limsupub  46987  limsupmnflem  47003  limsupre2lem  47007  limsuplt2  47036  liminfreuzlem  47085  liminfltlem  47087  liminflimsupclim  47090  xlimmnfmpt  47126  xlimpnfmpt  47127  fourierdlem73  47462  fourierdlem83  47472  meaiuninc3v  47767  ovolval2  47927  cfsetsnfsetfo  48403  dfaimafn  48508  iccelpart  48788  sprsymrelf  48850  sprsymrelfo  48852  nprmmul1  48882  nprmmul3  48884  fmtnoprmfac1  48923  fmtnoprmfac2  48925  fmtnofac2lem  48926  dfeven2  49020  dfodd3  49021  dfvopnbgr2  49224  usgrgrtrirex  49321  stgredgiun  49329  uspgrsprfo  49519  elbigo2  49995  rrxlinesc  50179  rrxlinec  50180  rrx2line  50183  rrx2vlinest  50184  itsclquadeu  50220