Theorem rexbidva 3184

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  rexbidv  3186  2rexbiia  3223  2rexbidva  3225  rexeqbidva  3326  frinxp  5734  onfr  6404  dfimafn  6950  funimass4  6952  fliftel  7319  fliftf  7325  isomin  7347  f1oiso  7361  releldm2  8056  fnwe2lem3  8151  oaass  8574  eldifsucnn  8678  cofonr  8688  naddunif  8708  qsinxp  8819  qliftel  8826  fimaxg  9283  ordunifi  9286  supisolem  9471  fiming  9497  wemapwe  9703  ttrcltr  9722  ttrclse  9733  frmin  9758  cflim2  10346  cfsmolem  10353  alephsing  10359  brdom7disj  10615  brdom6disj  10616  alephreg  10672  nqereu  11019  1idpr  11119  map2psrpr  11200  axsup  11390  rereccl  12040  sup3  12279  infm3  12281  supadd  12290  creur  12319  creui  12320  nndiv  12389  nnrecl  12609  rpnnen1lem2  13110  rpnnen1lem1  13111  rpnnen1lem3  13112  rpnnen1lem5  13114  supxrbnd1  13456  supxrbnd2  13457  supxrbnd  13463  rabssnn0fi  14134  mptnn0fsupp  14145  expnlbnd  14382  wrdl3s3  15122  limsuplt  15653  clim2  15678  clim2c  15679  clim0c  15681  ello12  15690  elo12  15701  rlimresb  15739  climabs0  15759  sumeq2ii  15867  mertens  16062  prodeq2ii  16087  zprod  16111  nndivides  16439  alzdvds  16497  oddm1even  16520  oddnn02np1  16525  oddge22np1  16526  evennn02n  16527  evennn2n  16528  divalglem4  16573  divalgb  16581  modremain  16585  modprmn0modprm0  16992  vdwlem6  17171  vdwlem11  17176  vdw  17179  ramval  17193  imasleval  17720  dfiso3  17955  fullestrcsetc  18332  fullsetcestrc  18347  isipodrs  18718  ipodrsfi  18720  mgmidpfod  18864  gsumpropd2lem  18875  mndpropd  18958  grppropd  19169  qus0subgbas  19420  conjnmzb  19474  symgextfo  19643  symgfixfo  19660  sylow1lem2  19820  sylow3lem1  19848  sylow3lem3  19850  lsmelvalm  19872  lsmass  19890  iscyg3  20107  ghmcyg  20117  cycsubgcyg  20122  pgpfac1lem2  20298  pgpfac1lem4  20301  ablfac2  20312  dvdsr02  20609  crngunit  20615  dvdsrpropd  20653  rngqiprngimfo  21604  lpigen  21666  pzriprnglem10  21803  znunit  21876  elfilspd  22116  psdmul  22494  scmatmats  22833  symgmatr01  22976  isclo  23412  iscnp3  23569  lmbrf  23585  cncnp  23605  lmss  23623  isnrm2  23683  cmpfi  23733  1stcfb  23770  1stccnp  23788  ptrescn  23965  txkgen  23978  xkoinjcn  24013  trfil3  24214  fmid  24286  lmflf  24331  txflf  24332  ptcmplem3  24380  tsmsf1o  24471  ucnprima  24607  metrest  24850  metcnp  24867  metcnp2  24868  txmetcnp  24873  metuel2  24891  metustbl  24892  psmetutop  24893  metucn  24897  evth2  25288  lmmbrf  25590  iscfil2  25594  fmcfil  25600  iscau2  25605  iscau4  25607  iscauf  25608  caucfil  25611  iscmet3lem3  25618  cfilresi  25623  causs  25626  lmclim  25631  ivth2  25783  ovolfioo  25795  ovolficc  25796  ovolshftlem1  25837  ovolscalem1  25841  volsup2  25933  ismbf3d  25982  mbfaddlem  25988  mbfsup  25992  mbfinf  25993  itg2seq  26070  itg2gt0  26088  ellimc2  26204  ellimc3  26206  rolle  26317  cmvth  26318  mvth  26319  dvlip  26320  dvivth  26337  lhop1lem  26340  deg1ldg  26417  rnplynfin  26637  plyconz  26638  ulm2  26719  ulmdvlem3  26736  dcubic  27181  mcubic  27182  cubic2  27183  rlimcnp  27300  ftalem3  27409  isppw2  27449  lgsquadlem2  27715  2lgslem1a  27725  dchrmusumlema  27827  dchrisum0lema  27848  infdesc  27974  cofcutr  28317  lrrecfr  28336  addsrid  28357  addscom  28359  addsuniflem  28394  addsass  28398  addbday  28411  negsunif  28448  mulsrid  28506  mulsasslem3  28558  n0s0suc  28735  z12sge0  28876  elreno2  28888  renegscl  28891  readdscl  28892  remulscllem2  28894  remulscl  28895  tglowdim2l  29126  mirreu3  29133  oppcom  29227  iscgra1  29324  axsegcon  29512  axpasch  29526  axcontlem7  29555  usgr2pth0  30358  usgr2wspthon  30564  elwwlks2  30565  elwspths2spth  30566  rusgrnumwwlks  30573  clwwlkfo  30648  eclclwwlkn1  30673  eucrctshift  30851  fusgreg2wsp  30944  nmobndi  31384  nmounbi  31385  nmoo0  31400  h2hcau  31588  h2hlm  31589  shsel3  31924  pjhtheu2  32025  chscllem2  32247  adjbdln  32692  branmfn  32714  pjimai  32785  chrelati  32973  cdj3lem3  33047  cdj3lem3b  33049  dfimafnf  33279  ofpreima  33308  isarchi2  33794  submarchi  33795  archirng  33797  archiabl  33807  isarchiofld  33808  isunitc  33850  ellspds  33972  dvdsruasso2  33989  lsmssass  34001  grplsm0l  34002  fedgmullem2  34310  elirng  34366  zarcls  34554  ordtconnlem1  34604  lmdvg  34633  esumfsup  34750  dya2icoseg2  34958  eulerpartlemgh  35058  ballotlemodife  35178  ballotlemsima  35196  nummin  35776  erdszelem10  36053  iscvm  36112  wsuclem  36681  seglelin  36975  outsideofeu  36990  ltnadd  37061  naddle  37062  opnrebl  37202  opnrebl2  37203  filnetlem4  37263  bj-finsumval0  38313  phpreu  38634  ptrest  38644  poimirlem3  38648  poimirlem4  38649  poimirlem17  38662  poimirlem26  38671  poimirlem27  38672  broucube  38679  mblfinlem1  38682  lmclim2  38799  caures  38801  isbnd3b  38826  heiborlem7  38858  heiborlem10  38861  rrncmslem  38873  isdrngo2  38999  erimeq2  39802  prter3  40046  islshpsm  40144  lsatfixedN  40173  lrelat  40178  eqlkr2  40264  lshpkrlem1  40274  lfl1dim  40285  eqlkr4  40329  ishlat3N  40518  hlsupr2  40551  hlrelat5N  40565  hlrelat  40566  cvrval5  40579  cvrat42  40608  athgt  40620  3dim0  40621  islln3  40674  llnexatN  40685  islpln3  40697  islvol3  40740  islvol5  40743  isline4N  40941  polval2N  41070  4atex3  41245  cdleme0ex2N  41388  cdlemefrs29cpre1  41562  cdlemb3  41770  cdlemg33c  41872  cdlemg33e  41874  dia1dim2  42226  cdlemm10N  42282  dib1dim2  42332  diclspsn  42358  dih1dimatlem  42493  dihatexv2  42503  djhcvat42  42579  dihjat1lem  42592  dvh4dimat  42602  dvh2dimatN  42604  lcfrlem9  42714  mapdval4N  42796  mapdcv  42824  ef11d  43497  cxp112d  43499  cxp111d  43500  sn-sup3d  43663  fimgmcyc  43705  elrfirn  43813  elrfirn2  43814  mrefg3  43826  diophin  43890  diophun  43891  diophren  43927  rmxycomplete  44031  wepwsolem  44156  islssfg  44179  unielss  44327  onmaxnelsup  44332  onsupnmax  44337  onsupeqnmax  44356  tfsconcat0i  44454  ntrneineine0lem  45190  ntrneineine1lem  45191  ntrneiel2  45193  extoimad  45271  grumnudlem  45376  modelac8prim  46089  supsubc  46472  infxrbnd2  46487  supminfxr  46581  evthiccabs  46615  elicores  46652  clim2f  46753  clim2cf  46767  clim0cf  46771  clim2f2  46787  limsupub  46821  limsupmnflem  46837  limsupre2lem  46841  limsuplt2  46870  liminfreuzlem  46919  liminfltlem  46921  liminflimsupclim  46924  xlimmnfmpt  46960  xlimpnfmpt  46961  fourierdlem73  47296  fourierdlem83  47306  meaiuninc3v  47601  ovolval2  47761  cfsetsnfsetfo  48237  dfaimafn  48342  iccelpart  48622  sprsymrelf  48684  sprsymrelfo  48686  nprmmul1  48716  nprmmul3  48718  fmtnoprmfac1  48757  fmtnoprmfac2  48759  fmtnofac2lem  48760  dfeven2  48854  dfodd3  48855  dfvopnbgr2  49058  usgrgrtrirex  49155  stgredgiun  49163  uspgrsprfo  49353  elbigo2  49771  rrxlinesc  49955  rrxlinec  49956  rrx2line  49959  rrx2vlinest  49960  itsclquadeu  49996