Theorem rexbidva 3193

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 589	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
3	2	rexbidv2 3191	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2149  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-rex 3096

This theorem is referenced by:  rexbidv  3195  2rexbiia  3232  2rexbidva  3234  rexeqbidva  3336  frinxp  5745  onfr  6401  dfimafn  6944  funimass4  6946  fliftel  7308  fliftf  7314  isomin  7336  f1oiso  7350  releldm2  8039  oaass  8545  eldifsucnn  8649  cofonr  8659  naddunif  8679  qsinxp  8790  qliftel  8797  fimaxg  9246  ordunifi  9249  supisolem  9433  fiming  9459  wemapwe  9665  ttrcltr  9684  ttrclse  9695  frmin  9720  cflim2  10246  cfsmolem  10253  alephsing  10259  brdom7disj  10514  brdom6disj  10515  alephreg  10566  nqereu  10913  1idpr  11013  map2psrpr  11094  axsup  11284  rereccl  11932  sup3  12171  infm3  12173  supadd  12182  creur  12211  creui  12212  nndiv  12281  nnrecl  12501  rpnnen1lem2  13000  rpnnen1lem1  13001  rpnnen1lem3  13002  rpnnen1lem5  13004  supxrbnd1  13346  supxrbnd2  13347  supxrbnd  13353  rabssnn0fi  14021  mptnn0fsupp  14032  expnlbnd  14268  wrdl3s3  14998  limsuplt  15529  clim2  15554  clim2c  15555  clim0c  15557  ello12  15566  elo12  15577  rlimresb  15615  climabs0  15635  sumeq2ii  15743  mertens  15939  prodeq2ii  15964  zprod  15990  nndivides  16319  alzdvds  16377  oddm1even  16400  oddnn02np1  16405  oddge22np1  16406  evennn02n  16407  evennn2n  16408  divalglem4  16453  divalgb  16461  modremain  16465  modprmn0modprm0  16866  vdwlem6  17045  vdwlem11  17050  vdw  17053  ramval  17067  imasleval  17594  dfiso3  17829  fullestrcsetc  18206  fullsetcestrc  18221  isipodrs  18592  ipodrsfi  18594  gsumpropd2lem  18736  mndpropd  18816  grppropd  19017  qus0subgbas  19268  conjnmzb  19322  symgextfo  19491  symgfixfo  19508  sylow1lem2  19668  sylow3lem1  19696  sylow3lem3  19698  lsmelvalm  19720  lsmass  19738  iscyg3  19955  ghmcyg  19965  cycsubgcyg  19970  pgpfac1lem2  20146  pgpfac1lem4  20149  ablfac2  20160  dvdsr02  20453  crngunit  20459  dvdsrpropd  20497  rngqiprngimfo  21411  lpigen  21471  pzriprnglem10  21608  znunit  21681  elfilspd  21921  psdmul  22297  scmatmats  22636  symgmatr01  22779  isclo  23212  iscnp3  23369  lmbrf  23385  cncnp  23405  lmss  23423  isnrm2  23483  cmpfi  23533  1stcfb  23570  1stccnp  23587  ptrescn  23764  txkgen  23777  xkoinjcn  23812  trfil3  24013  fmid  24085  lmflf  24130  txflf  24131  ptcmplem3  24179  tsmsf1o  24270  ucnprima  24406  metrest  24649  metcnp  24666  metcnp2  24667  txmetcnp  24672  metuel2  24690  metustbl  24691  psmetutop  24692  metucn  24696  evth2  25087  lmmbrf  25389  iscfil2  25393  fmcfil  25399  iscau2  25404  iscau4  25406  iscauf  25407  caucfil  25410  iscmet3lem3  25417  cfilresi  25422  causs  25425  lmclim  25430  ivth2  25582  ovolfioo  25594  ovolficc  25595  ovolshftlem1  25636  ovolscalem1  25640  volsup2  25732  ismbf3d  25781  mbfaddlem  25787  mbfsup  25791  mbfinf  25792  itg2seq  25869  itg2gt0  25887  ellimc2  26004  ellimc3  26006  rolle  26117  cmvth  26118  mvth  26119  dvlip  26120  dvivth  26137  lhop1lem  26140  deg1ldg  26217  ulm2  26513  ulmdvlem3  26530  dcubic  26976  mcubic  26977  cubic2  26978  rlimcnp  27095  ftalem3  27204  isppw2  27244  lgsquadlem2  27510  2lgslem1a  27520  dchrmusumlema  27622  dchrisum0lema  27643  cofcutr  28082  lrrecfr  28101  addsrid  28122  addscom  28124  addsuniflem  28159  addsass  28163  addbday  28176  negsunif  28213  mulsrid  28271  mulsasslem3  28323  n0s0suc  28500  z12sge0  28641  elreno2  28653  renegscl  28656  readdscl  28657  remulscllem2  28659  remulscl  28660  tglowdim2l  28885  mirreu3  28892  oppcom  28983  iscgra1  29077  axsegcon  29217  axpasch  29231  axcontlem7  29260  usgr2pth0  30054  usgr2wspthon  30257  elwwlks2  30258  elwspths2spth  30259  rusgrnumwwlks  30266  clwwlkfo  30341  eclclwwlkn1  30366  eucrctshift  30534  fusgreg2wsp  30627  nmobndi  31067  nmounbi  31068  nmoo0  31083  h2hcau  31271  h2hlm  31272  shsel3  31607  pjhtheu2  31708  chscllem2  31930  adjbdln  32375  branmfn  32397  pjimai  32468  chrelati  32656  cdj3lem3  32730  cdj3lem3b  32732  dfimafnf  32921  ofpreima  32950  isarchi2  33445  submarchi  33446  archirng  33448  archiabl  33458  isarchiofld  33459  isunitc  33501  ellspds  33625  dvdsruasso2  33642  lsmssass  33654  grplsm0l  33655  fedgmullem2  33964  elirng  34020  zarcls  34208  ordtconnlem1  34258  lmdvg  34287  esumfsup  34404  dya2icoseg2  34612  eulerpartlemgh  34712  ballotlemodife  34832  ballotlemsima  34850  nummin  35426  erdszelem10  35590  iscvm  35649  wsuclem  36213  seglelin  36506  outsideofeu  36521  opnrebl  36719  opnrebl2  36720  filnetlem4  36780  bj-finsumval0  37816  phpreu  38142  ptrest  38157  poimirlem3  38161  poimirlem4  38162  poimirlem17  38175  poimirlem26  38184  poimirlem27  38185  broucube  38192  mblfinlem1  38195  lmclim2  38296  caures  38298  isbnd3b  38323  heiborlem7  38355  heiborlem10  38358  rrncmslem  38370  isdrngo2  38496  erimeq2  39301  prter3  39545  islshpsm  39643  lsatfixedN  39672  lrelat  39677  eqlkr2  39763  lshpkrlem1  39773  lfl1dim  39784  eqlkr4  39828  ishlat3N  40017  hlsupr2  40050  hlrelat5N  40064  hlrelat  40065  cvrval5  40078  cvrat42  40107  athgt  40119  3dim0  40120  islln3  40173  llnexatN  40184  islpln3  40196  islvol3  40239  islvol5  40242  isline4N  40440  polval2N  40569  4atex3  40744  cdleme0ex2N  40887  cdlemefrs29cpre1  41061  cdlemb3  41269  cdlemg33c  41371  cdlemg33e  41373  dia1dim2  41725  cdlemm10N  41781  dib1dim2  41831  diclspsn  41857  dih1dimatlem  41992  dihatexv2  42002  djhcvat42  42078  dihjat1lem  42091  dvh4dimat  42101  dvh2dimatN  42103  lcfrlem9  42213  mapdval4N  42295  mapdcv  42323  ef11d  42989  cxp112d  42991  cxp111d  42992  sn-sup3d  43155  fimgmcyc  43193  infdesc  43266  elrfirn  43317  elrfirn2  43318  mrefg3  43330  diophin  43394  diophun  43395  diophren  43431  rmxycomplete  43535  wepwsolem  43660  fnwe2lem2  43669  islssfg  43688  unielss  43836  onmaxnelsup  43841  onsupnmax  43846  onsupeqnmax  43865  tfsconcat0i  43963  ntrneineine0lem  44700  ntrneineine1lem  44701  ntrneiel2  44703  extoimad  44781  grumnudlem  44886  modelac8prim  45592  supsubc  45960  infxrbnd2  45975  supminfxr  46069  evthiccabs  46103  elicores  46140  clim2f  46241  clim2cf  46255  clim0cf  46259  clim2f2  46275  limsupub  46309  limsupmnflem  46325  limsupre2lem  46329  limsuplt2  46358  liminfreuzlem  46407  liminfltlem  46409  liminflimsupclim  46412  xlimmnfmpt  46448  xlimpnfmpt  46449  fourierdlem73  46784  fourierdlem83  46794  meaiuninc3v  47089  ovolval2  47249  cfsetsnfsetfo  47685  dfaimafn  47790  iccelpart  48070  sprsymrelf  48132  sprsymrelfo  48134  nprmmul1  48164  nprmmul3  48166  fmtnoprmfac1  48205  fmtnoprmfac2  48207  fmtnofac2lem  48208  dfeven2  48302  dfodd3  48303  dfvopnbgr2  48506  usgrgrtrirex  48603  stgredgiun  48611  uspgrsprfo  48801  elbigo2  49216  rrxlinesc  49399  rrxlinec  49400  rrx2line  49404  rrx2vlinest  49405  itsclquadeu  49441