Theorem rexbidva 3186

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

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

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 3089

This theorem is used by:  rexbidv  3188  2rexbiia  3225  2rexbidva  3227  rexeqbidva  3328  frinxp  5742  onfr  6401  dfimafn  6944  funimass4  6946  fliftel  7313  fliftf  7319  isomin  7341  f1oiso  7355  releldm2  8043  oaass  8551  eldifsucnn  8655  cofonr  8665  naddunif  8685  qsinxp  8796  qliftel  8803  fimaxg  9260  ordunifi  9263  supisolem  9447  fiming  9473  wemapwe  9679  ttrcltr  9698  ttrclse  9709  frmin  9734  cflim2  10268  cfsmolem  10275  alephsing  10281  brdom7disj  10537  brdom6disj  10538  alephreg  10594  nqereu  10941  1idpr  11041  map2psrpr  11122  axsup  11312  rereccl  11960  sup3  12199  infm3  12201  supadd  12210  creur  12239  creui  12240  nndiv  12309  nnrecl  12529  rpnnen1lem2  13029  rpnnen1lem1  13030  rpnnen1lem3  13031  rpnnen1lem5  13033  supxrbnd1  13375  supxrbnd2  13376  supxrbnd  13382  rabssnn0fi  14052  mptnn0fsupp  14063  expnlbnd  14299  wrdl3s3  15037  limsuplt  15568  clim2  15593  clim2c  15594  clim0c  15596  ello12  15605  elo12  15616  rlimresb  15654  climabs0  15674  sumeq2ii  15782  mertens  15977  prodeq2ii  16002  zprod  16028  nndivides  16356  alzdvds  16414  oddm1even  16437  oddnn02np1  16442  oddge22np1  16443  evennn02n  16444  evennn2n  16445  divalglem4  16490  divalgb  16498  modremain  16502  modprmn0modprm0  16903  vdwlem6  17082  vdwlem11  17087  vdw  17090  ramval  17104  imasleval  17631  dfiso3  17866  fullestrcsetc  18243  fullsetcestrc  18258  isipodrs  18629  ipodrsfi  18631  mgmidpfod  18774  gsumpropd2lem  18785  mndpropd  18868  grppropd  19079  qus0subgbas  19330  conjnmzb  19384  symgextfo  19553  symgfixfo  19570  sylow1lem2  19730  sylow3lem1  19758  sylow3lem3  19760  lsmelvalm  19782  lsmass  19800  iscyg3  20017  ghmcyg  20027  cycsubgcyg  20032  pgpfac1lem2  20208  pgpfac1lem4  20211  ablfac2  20222  dvdsr02  20517  crngunit  20523  dvdsrpropd  20561  rngqiprngimfo  21508  lpigen  21570  pzriprnglem10  21707  znunit  21780  elfilspd  22020  psdmul  22398  scmatmats  22737  symgmatr01  22880  isclo  23316  iscnp3  23473  lmbrf  23489  cncnp  23509  lmss  23527  isnrm2  23587  cmpfi  23637  1stcfb  23674  1stccnp  23692  ptrescn  23869  txkgen  23882  xkoinjcn  23917  trfil3  24118  fmid  24190  lmflf  24235  txflf  24236  ptcmplem3  24284  tsmsf1o  24375  ucnprima  24511  metrest  24754  metcnp  24771  metcnp2  24772  txmetcnp  24777  metuel2  24795  metustbl  24796  psmetutop  24797  metucn  24801  evth2  25192  lmmbrf  25494  iscfil2  25498  fmcfil  25504  iscau2  25509  iscau4  25511  iscauf  25512  caucfil  25515  iscmet3lem3  25522  cfilresi  25527  causs  25530  lmclim  25535  ivth2  25687  ovolfioo  25699  ovolficc  25700  ovolshftlem1  25741  ovolscalem1  25745  volsup2  25837  ismbf3d  25886  mbfaddlem  25892  mbfsup  25896  mbfinf  25897  itg2seq  25974  itg2gt0  25992  ellimc2  26109  ellimc3  26111  rolle  26222  cmvth  26223  mvth  26224  dvlip  26225  dvivth  26242  lhop1lem  26245  deg1ldg  26322  ulm2  26621  ulmdvlem3  26638  dcubic  27084  mcubic  27085  cubic2  27086  rlimcnp  27203  ftalem3  27312  isppw2  27352  lgsquadlem2  27618  2lgslem1a  27628  dchrmusumlema  27730  dchrisum0lema  27751  cofcutr  28190  lrrecfr  28209  addsrid  28230  addscom  28232  addsuniflem  28267  addsass  28271  addbday  28284  negsunif  28321  mulsrid  28379  mulsasslem3  28431  n0s0suc  28608  z12sge0  28749  elreno2  28761  renegscl  28764  readdscl  28765  remulscllem2  28767  remulscl  28768  tglowdim2l  28999  mirreu3  29006  oppcom  29100  iscgra1  29197  axsegcon  29385  axpasch  29399  axcontlem7  29428  usgr2pth0  30231  usgr2wspthon  30437  elwwlks2  30438  elwspths2spth  30439  rusgrnumwwlks  30446  clwwlkfo  30521  eclclwwlkn1  30546  eucrctshift  30724  fusgreg2wsp  30817  nmobndi  31257  nmounbi  31258  nmoo0  31273  h2hcau  31461  h2hlm  31462  shsel3  31797  pjhtheu2  31898  chscllem2  32120  adjbdln  32565  branmfn  32587  pjimai  32658  chrelati  32846  cdj3lem3  32920  cdj3lem3b  32922  dfimafnf  33111  ofpreima  33140  isarchi2  33627  submarchi  33628  archirng  33630  archiabl  33640  isarchiofld  33641  isunitc  33683  ellspds  33805  dvdsruasso2  33821  lsmssass  33833  grplsm0l  33834  fedgmullem2  34142  elirng  34198  zarcls  34386  ordtconnlem1  34436  lmdvg  34465  esumfsup  34582  dya2icoseg2  34791  eulerpartlemgh  34891  ballotlemodife  35011  ballotlemsima  35029  nummin  35600  erdszelem10  35781  iscvm  35840  wsuclem  36404  seglelin  36698  outsideofeu  36713  ltnadd  36800  naddle  36801  opnrebl  36941  opnrebl2  36942  filnetlem4  37002  bj-finsumval0  38039  phpreu  38360  ptrest  38370  poimirlem3  38374  poimirlem4  38375  poimirlem17  38388  poimirlem26  38397  poimirlem27  38398  broucube  38405  mblfinlem1  38408  lmclim2  38510  caures  38512  isbnd3b  38537  heiborlem7  38569  heiborlem10  38572  rrncmslem  38584  isdrngo2  38710  erimeq2  39513  prter3  39757  islshpsm  39855  lsatfixedN  39884  lrelat  39889  eqlkr2  39975  lshpkrlem1  39985  lfl1dim  39996  eqlkr4  40040  ishlat3N  40229  hlsupr2  40262  hlrelat5N  40276  hlrelat  40277  cvrval5  40290  cvrat42  40319  athgt  40331  3dim0  40332  islln3  40385  llnexatN  40396  islpln3  40408  islvol3  40451  islvol5  40454  isline4N  40652  polval2N  40781  4atex3  40956  cdleme0ex2N  41099  cdlemefrs29cpre1  41273  cdlemb3  41481  cdlemg33c  41583  cdlemg33e  41585  dia1dim2  41937  cdlemm10N  41993  dib1dim2  42043  diclspsn  42069  dih1dimatlem  42204  dihatexv2  42214  djhcvat42  42290  dihjat1lem  42303  dvh4dimat  42313  dvh2dimatN  42315  lcfrlem9  42425  mapdval4N  42507  mapdcv  42535  ef11d  43216  cxp112d  43218  cxp111d  43219  sn-sup3d  43382  fimgmcyc  43418  infdesc  43491  elrfirn  43542  elrfirn2  43543  mrefg3  43555  diophin  43619  diophun  43620  diophren  43656  rmxycomplete  43760  wepwsolem  43885  fnwe2lem2  43894  islssfg  43913  unielss  44061  onmaxnelsup  44066  onsupnmax  44071  onsupeqnmax  44090  tfsconcat0i  44188  ntrneineine0lem  44925  ntrneineine1lem  44926  ntrneiel2  44928  extoimad  45006  grumnudlem  45111  modelac8prim  45817  supsubc  46185  infxrbnd2  46200  supminfxr  46294  evthiccabs  46328  elicores  46365  clim2f  46466  clim2cf  46480  clim0cf  46484  clim2f2  46500  limsupub  46534  limsupmnflem  46550  limsupre2lem  46554  limsuplt2  46583  liminfreuzlem  46632  liminfltlem  46634  liminflimsupclim  46637  xlimmnfmpt  46673  xlimpnfmpt  46674  fourierdlem73  47009  fourierdlem83  47019  meaiuninc3v  47314  ovolval2  47474  cfsetsnfsetfo  47950  dfaimafn  48055  iccelpart  48335  sprsymrelf  48397  sprsymrelfo  48399  nprmmul1  48429  nprmmul3  48431  fmtnoprmfac1  48470  fmtnoprmfac2  48472  fmtnofac2lem  48473  dfeven2  48567  dfodd3  48568  dfvopnbgr2  48771  usgrgrtrirex  48868  stgredgiun  48876  uspgrsprfo  49066  elbigo2  49484  rrxlinesc  49667  rrxlinec  49668  rrx2line  49672  rrx2vlinest  49673  itsclquadeu  49709