Theorem rexbidva 3183

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  rexbidv  3185  2rexbiia  3224  2rexbidva  3226  rexeqbidva  3341  frinxp  5782  onfr  6434  dfimafn  6984  funimass4  6986  fliftel  7345  fliftf  7351  isomin  7373  f1oiso  7387  releldm2  8084  oaass  8617  eldifsucnn  8720  cofonr  8730  naddunif  8749  qsinxp  8851  qliftel  8858  fimaxg  9351  ordunifi  9354  supisolem  9542  fiming  9567  wemapwe  9766  ttrcltr  9785  ttrclse  9796  frmin  9818  cflim2  10332  cfsmolem  10339  alephsing  10345  brdom7disj  10600  brdom6disj  10601  alephreg  10651  nqereu  10998  1idpr  11098  map2psrpr  11179  axsup  11365  rereccl  12012  sup3  12252  infm3  12254  supadd  12263  creur  12287  creui  12288  nndiv  12339  nnrecl  12551  rpnnen1lem2  13042  rpnnen1lem1  13043  rpnnen1lem3  13044  rpnnen1lem5  13046  supxrbnd1  13383  supxrbnd2  13384  supxrbnd  13390  rabssnn0fi  14037  mptnn0fsupp  14048  expnlbnd  14282  wrdl3s3  15011  limsuplt  15525  clim2  15550  clim2c  15551  clim0c  15553  ello12  15562  elo12  15573  rlimresb  15611  climabs0  15631  sumeq2ii  15741  mertens  15934  prodeq2ii  15959  zprod  15985  nndivides  16312  alzdvds  16368  oddm1even  16391  oddnn02np1  16396  oddge22np1  16397  evennn02n  16398  evennn2n  16399  divalglem4  16444  divalgb  16452  modremain  16456  modprmn0modprm0  16854  vdwlem6  17033  vdwlem11  17038  vdw  17041  ramval  17055  imasleval  17601  dfiso3  17834  fullestrcsetc  18220  fullsetcestrc  18235  isipodrs  18607  ipodrsfi  18609  gsumpropd2lem  18717  mndpropd  18797  grppropd  18991  qus0subgbas  19238  conjnmzb  19293  symgextfo  19464  symgfixfo  19481  sylow1lem2  19641  sylow3lem1  19669  sylow3lem3  19671  lsmelvalm  19693  lsmass  19711  iscyg3  19928  ghmcyg  19938  cycsubgcyg  19943  pgpfac1lem2  20119  pgpfac1lem4  20122  ablfac2  20133  dvdsr02  20398  crngunit  20404  dvdsrpropd  20442  rngqiprngimfo  21334  lpigen  21368  pzriprnglem10  21524  znunit  21605  elfilspd  21846  psdmul  22193  scmatmats  22538  symgmatr01  22681  isclo  23116  iscnp3  23273  lmbrf  23289  cncnp  23309  lmss  23327  isnrm2  23387  cmpfi  23437  1stcfb  23474  1stccnp  23491  ptrescn  23668  txkgen  23681  xkoinjcn  23716  trfil3  23917  fmid  23989  lmflf  24034  txflf  24035  ptcmplem3  24083  tsmsf1o  24174  ucnprima  24312  metrest  24558  metcnp  24575  metcnp2  24576  txmetcnp  24581  metuel2  24599  metustbl  24600  psmetutop  24601  metucn  24605  evth2  25011  lmmbrf  25315  iscfil2  25319  fmcfil  25325  iscau2  25330  iscau4  25332  iscauf  25333  caucfil  25336  iscmet3lem3  25343  cfilresi  25348  causs  25351  lmclim  25356  ivth2  25509  ovolfioo  25521  ovolficc  25522  ovolshftlem1  25563  ovolscalem1  25567  volsup2  25659  ismbf3d  25708  mbfaddlem  25714  mbfsup  25718  mbfinf  25719  itg2seq  25797  itg2gt0  25815  ellimc2  25932  ellimc3  25934  rolle  26048  cmvth  26049  cmvthOLD  26050  mvth  26051  dvlip  26052  dvivth  26069  lhop1lem  26072  deg1ldg  26151  ulm2  26446  ulmdvlem3  26463  dcubic  26907  mcubic  26908  cubic2  26909  rlimcnp  27026  ftalem3  27136  isppw2  27176  lgsquadlem2  27443  2lgslem1a  27453  dchrmusumlema  27555  dchrisum0lema  27576  cofcutr  27976  lrrecfr  27994  addsrid  28015  addscom  28017  addsuniflem  28052  addsass  28056  addsbday  28068  negsunif  28105  mulsrid  28157  mulsasslem3  28209  n0s0suc  28363  renegscl  28448  readdscl  28449  remulscllem2  28451  remulscl  28452  tglowdim2l  28676  mirreu3  28680  oppcom  28770  iscgra1  28836  axsegcon  28960  axpasch  28974  axcontlem7  29003  usgr2pth0  29801  usgr2wspthon  29998  elwwlks2  29999  elwspths2spth  30000  rusgrnumwwlks  30007  clwwlkfo  30082  eclclwwlkn1  30107  eucrctshift  30275  fusgreg2wsp  30368  nmobndi  30807  nmounbi  30808  nmoo0  30823  h2hcau  31011  h2hlm  31012  shsel3  31347  pjhtheu2  31448  chscllem2  31670  adjbdln  32115  branmfn  32137  pjimai  32208  chrelati  32396  cdj3lem3  32470  cdj3lem3b  32472  dfimafnf  32655  ofpreima  32683  isarchi2  33165  submarchi  33166  archirng  33168  archiabl  33178  isarchiofld  33312  ellspds  33361  dvdsruasso2  33379  lsmssass  33395  grplsm0l  33396  fedgmullem2  33643  elirng  33686  zarcls  33820  ordtconnlem1  33870  lmdvg  33899  esumfsup  34034  dya2icoseg2  34243  eulerpartlemgh  34343  ballotlemodife  34462  ballotlemsima  34480  nummin  35067  erdszelem10  35168  iscvm  35227  wsuclem  35789  seglelin  36080  outsideofeu  36095  opnrebl  36286  opnrebl2  36287  filnetlem4  36347  bj-finsumval0  37251  phpreu  37564  ptrest  37579  poimirlem3  37583  poimirlem4  37584  poimirlem17  37597  poimirlem26  37606  poimirlem27  37607  broucube  37614  mblfinlem1  37617  lmclim2  37718  caures  37720  isbnd3b  37745  heiborlem7  37777  heiborlem10  37780  rrncmslem  37792  isdrngo2  37918  erimeq2  38634  prter3  38838  islshpsm  38936  lsatfixedN  38965  lrelat  38970  eqlkr2  39056  lshpkrlem1  39066  lfl1dim  39077  eqlkr4  39121  ishlat3N  39310  hlsupr2  39344  hlrelat5N  39358  hlrelat  39359  cvrval5  39372  cvrat42  39401  athgt  39413  3dim0  39414  islln3  39467  llnexatN  39478  islpln3  39490  islvol3  39533  islvol5  39536  isline4N  39734  polval2N  39863  4atex3  40038  cdleme0ex2N  40181  cdlemefrs29cpre1  40355  cdlemb3  40563  cdlemg33c  40665  cdlemg33e  40667  dia1dim2  41019  cdlemm10N  41075  dib1dim2  41125  diclspsn  41151  dih1dimatlem  41286  dihatexv2  41296  djhcvat42  41372  dihjat1lem  41385  dvh4dimat  41395  dvh2dimatN  41397  lcfrlem9  41507  mapdval4N  41589  mapdcv  41617  ef11d  42327  cxp112d  42329  cxp111d  42330  sn-sup3d  42448  fimgmcyc  42489  infdesc  42598  elrfirn  42651  elrfirn2  42652  mrefg3  42664  diophin  42728  diophun  42729  diophren  42769  rmxycomplete  42874  wepwsolem  42999  fnwe2lem2  43008  islssfg  43027  unielss  43179  onmaxnelsup  43184  onsupnmax  43189  onsupeqnmax  43208  tfsconcat0i  43307  ntrneineine0lem  44045  ntrneineine1lem  44046  ntrneiel2  44048  extoimad  44126  grumnudlem  44254  supsubc  45268  infxrbnd2  45284  supminfxr  45379  evthiccabs  45414  elicores  45451  clim2f  45557  clim2cf  45571  clim0cf  45575  clim2f2  45591  limsupub  45625  limsupmnflem  45641  limsupre2lem  45645  limsuplt2  45674  liminfreuzlem  45723  liminfltlem  45725  liminflimsupclim  45728  xlimmnfmpt  45764  xlimpnfmpt  45765  fourierdlem73  46100  fourierdlem83  46110  meaiuninc3v  46405  ovolval2  46565  cfsetsnfsetfo  46975  dfaimafn  47080  iccelpart  47307  sprsymrelf  47369  sprsymrelfo  47371  fmtnoprmfac1  47439  fmtnoprmfac2  47441  fmtnofac2lem  47442  dfeven2  47523  dfodd3  47524  dfvopnbgr2  47725  usgrgrtrirex  47799  uspgrsprfo  47871  elbigo2  48286  rrxlinesc  48469  rrxlinec  48470  rrx2line  48474  rrx2vlinest  48475  itsclquadeu  48511