Theorem rexbidv 3242

Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 6-Dec-2019.)

Hypothesis

Ref	Expression
rexbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rexbidv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rexbidv

Step	Hyp	Ref	Expression
1		rexbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	adantr 473	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	rexbidva 3241	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 198   ∈ wcel 2050  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-rex 3094

This theorem is referenced by:  2rexbidv  3245  rexralbidv  3246  rexeqbi1dvOLD  3358  rexeqbidvOLD  3364  cbvrex2v  3393  rspc2ev  3550  rspc3ev  3552  ceqsrex2v  3565  reuxfr4d  3654  uniiunlem  3953  n0snor2el  4639  eliun  4797  dfiin2g  4828  dfiunv2  4831  elrnmpt  5672  elrnmptg  5675  elimag  5776  fvelrnb  6558  fvelimab  6568  foelrn  6697  foco2  6698  elabrex  6829  abrexco  6830  f1oiso  6929  f1oiso2  6930  grprinvlem  7204  orduninsuc  7376  funcnvuni  7453  fun11iun  7460  abrexex2g  7479  f1oweALT  7487  el2xptp  7549  tfrlem12  7831  seqomlem2  7892  nneob  8081  qseq2  8146  elqsg  8150  elqsecl  8153  elixpsn  8300  ixpsnf1o  8301  isfi  8332  enfi  8531  pssnn  8533  frfi  8560  unblem1  8567  unblem2  8568  unbnn2  8572  fofinf1o  8596  finsschain  8628  indexfi  8629  elfi  8674  marypha1lem  8694  supeq3  8710  supmo  8713  suplub  8721  supisolem  8734  eqinf  8745  infval  8747  infglb  8751  infglbb  8752  infmo  8756  oieq1  8773  ordtypelem2  8780  ordtypelem3  8781  ordtypelem9  8787  wemaplem1  8807  brwdom2  8834  brwdom3  8843  unwdomg  8845  oemapval  8942  cantnf  8952  wemapwe  8956  cnfcom3clem  8964  tz9.13  9016  tz9.13g  9017  cardf2  9168  isnum2  9170  ennum  9172  cardiun  9207  infxpenc2  9244  aceq1  9339  aceq2  9341  dfac5lem3  9347  dfac5lem4  9348  dfac2a  9351  dfac2b  9352  kmlem9  9380  kmlem12  9383  kmlem14  9385  ackbij1  9460  cflm  9472  cfss  9487  cofsmo  9491  cfsmolem  9492  cfcoflem  9494  coftr  9495  isfin7  9523  fin23lem26  9547  isf32lem5  9579  fin1a2lem11  9632  hsmexlem2  9649  axdc3lem3  9674  axdc3  9676  numthcor  9716  zorn2lem7  9724  brdom3  9750  brdom7disj  9753  brdom6disj  9754  iundom2g  9762  fpwwe2  9865  winainflem  9915  winalim2  9918  inar1  9997  tskuni  10005  nqereu  10151  prnmax  10217  genpv  10221  genpnmax  10229  genpass  10231  prlem936  10269  recexsrlem  10325  map2psrpr  10332  supsrlem  10333  axrrecex  10385  axpre-sup  10391  dedekind  10605  cnegex  10623  recex  11075  fimaxre3  11390  infm3  11403  supaddc  11411  supadd  11412  supmul1  11413  supmullem1  11414  supmullem2  11415  supmul  11416  creur  11435  creui  11436  cju  11437  nnunb  11706  arch  11707  xrsupsslem  12519  xrinfmsslem  12520  xrsupss  12521  xrinfmss  12522  xrub  12524  supxrunb1  12531  supxrunb2  12532  infmremnf  12555  infmrp1  12556  modmuladd  13099  fsequb2  13162  hashge2el2difr  13653  iswrd  13677  wrdval  13678  csbwrdg  13709  cshword  14016  0csh0  14019  0csh0OLD  14020  2cshwcshw  14052  scshwfzeqfzo  14053  cshimadifsn  14056  shftfval  14293  abs1m  14559  rexfiuz  14571  reusq0  14686  limsupbnd2  14704  clim  14715  rlim  14716  rlim2  14717  rlim0  14729  rlim0lt  14730  ello1mpt2  14743  o1lo1  14758  o1compt  14808  rlimdiv  14866  climsup  14890  sumeq1  14909  sumeq2w  14912  summo  14937  fsum  14940  fsumcvg3  14949  infcvgaux2i  15076  mertenslem1  15103  mertenslem2  15104  mertens  15105  prodeq1f  15125  prodeq2w  15129  prodmo  15153  fprod  15158  divides  15472  odd2np1lem  15552  opeo  15577  omeo  15578  divalglem4  15610  divalglem10  15616  divalg  15617  gcdcllem3  15713  zeqzmulgcd  15722  bezoutlem1  15746  exprmfct  15907  nnnn0modprm0  16002  pythagtriplem2  16013  pythagtrip  16030  pceu  16042  pcprmpw2  16077  unbenlem  16103  4sqlem12  16151  vdwapval  16168  vdwapun  16169  vdwmc2  16174  vdwpc  16175  vdwlem2  16177  vdwlem10  16185  vdwlem13  16188  vdwnnlem1  16190  rami  16210  cshwsiun  16292  cshwrepswhash1  16295  brssc  16945  isdrs  17405  drsdir  17406  drsdirfi  17409  isdrs2  17410  ipodrsima  17636  gsumvalx  17741  gsumpropd  17743  gsumress  17747  isnsgrp  17759  sgrp2nmndlem5  17888  grpinvex  17904  dfgrp2  17919  grpidinv2  17948  grpidinv  17949  dfgrp3lem  17987  grp1  17996  imasgrp2  18004  conjnmzb  18167  gaorb  18211  orbsta  18217  symgfix2  18308  symgextfo  18314  pmtrprfvalrn  18380  psgnunilem3  18389  psgneu  18399  psgnval  18400  psgnvali  18401  psgnvalii  18402  ispgp  18481  subgpgp  18486  sylow1  18492  pgpfi  18494  sylow2blem3  18511  fislw  18514  sylow3lem2  18517  lsmelvalm  18540  lsmass  18557  pj1fval  18581  pj1val  18582  pj1eu  18583  pj1id  18586  efgrelexlema  18638  efgrelexlemb  18639  efgredeu  18641  cyggeninv  18761  cygabl  18768  pgpfac1lem2  18950  pgpfac1lem3  18952  pgpfac1lem4  18953  pgpfac1  18955  pgpfaclem2  18957  pgpfac  18959  dvdsrval  19121  dvdsr  19122  subrgdvds  19275  lss1d  19460  lspsn  19499  lspsnel  19500  lspsolvlem  19639  rspsn  19751  opsrval  19971  znf1o  20403  cygznlem3  20421  psgndiflemA  20450  ellspd  20651  mat1dimelbas  20787  mat1dimbas  20788  scmatval  20820  scmatel  20821  scmateALT  20828  mat0scmat  20854  decpmataa0  21083  decpmatmulsumfsupp  21088  pmatcollpw2lem  21092  pm2mpmhmlem1  21133  chpscmat  21157  basis2  21266  eltg2  21273  tg2  21280  isclo  21402  neival  21417  isnei  21418  isneip  21420  restbas  21473  neitr  21495  cnpval  21551  iscnp  21552  cnpimaex  21571  lmbr  21573  lmbr2  21574  cnprest2  21605  lmff  21616  regsep  21649  pnrmopn  21658  nrmsep3  21670  isnrm2  21673  iscmp  21703  cmpsublem  21714  cmpsub  21715  tgcmp  21716  sscmp  21720  hauscmplem  21721  1stcclb  21759  1stcfb  21760  is2ndc  21761  2ndc1stc  21766  1stcrest  21768  2ndcctbss  21770  1stcelcls  21776  llyeq  21785  nllyeq  21786  hausllycmp  21809  lly1stc  21811  refssex  21826  refun0  21830  islocfin  21832  locfinnei  21838  comppfsc  21847  txbas  21882  ptval  21885  ptpjopn  21927  ptclsg  21930  txcnp  21935  ptcnp  21937  txrest  21946  ptrescn  21954  txcmp  21958  tx1stc  21965  xkococn  21975  kqreglem1  22056  fbasssin  22151  fbssfi  22152  fbssint  22153  fbun  22155  fgss2  22189  fgcl  22193  ufli  22229  fmfnfmlem3  22271  fbflim2  22292  hauspwpwf1  22302  flfneii  22307  flftg  22311  txflf  22321  fclscf  22340  alexsubb  22361  alexsubALT  22366  tsmssubm  22457  ustincl  22522  ustdiag  22523  ustinvel  22524  ustexhalf  22525  ust0  22534  trust  22544  elutop  22548  ucnval  22592  ucncn  22600  cfiluexsm  22605  cfiluweak  22610  blssps  22740  blss  22741  imasf1oxms  22805  mopni  22808  metss  22824  metrest  22840  metcnp3  22856  cfilucfil  22875  metuel2  22881  nlmvscn  23002  nrginvrcn  23007  icccmplem1  23136  icccmplem2  23137  icccmp  23139  divcn  23182  cncfval  23202  elcncf2  23204  cncfmet  23222  cnheibor  23265  evth  23269  lebnumlem3  23273  lebnum  23274  xlebnum  23275  lebnumii  23276  ipcn  23555  lmmbr  23567  lmmbr2  23568  cfilfval  23573  cfili  23577  iscfil3  23582  caufval  23584  iscau  23585  iscau2  23586  equivcfil  23608  equivcau  23609  lmcau  23622  ovolval  23780  elovolm  23782  ovolgelb  23787  ovoliunlem1  23809  ovoliun2  23813  ovolshftlem1  23816  ovolscalem1  23820  ovolicc  23830  ioombl1lem4  23868  uniioombllem2  23890  mbfaddlem  23967  mbfsup  23971  mbfinf  23972  mbflimsup  23973  i1fmulc  24010  itg1climres  24021  itg2val  24035  itg2l  24036  itg2leub  24041  itg2seq  24049  itg2monolem1  24057  itg2mono  24060  itg2i1fseq2  24063  cniccibl  24147  ellimc3  24183  limciun  24198  dvferm1  24288  dvferm2  24290  lhop1lem  24316  ply1divex  24436  ig1peu  24471  plyval  24489  elply2  24492  coeval  24519  coeeu  24521  coelem  24522  coeeq  24523  plydivlem4  24591  plydivex  24592  aannenlem2  24624  aalioulem2  24628  aaliou2  24635  ulmval  24674  ulm2  24679  ulmcau  24689  ulmdvlem3  24696  abelthlem9  24734  abelth  24735  efif1olem4  24833  eflogeq  24889  efopn  24945  cxpcn3  25033  cxpeq  25042  rlimcnp  25248  lgamgulmlem6  25316  muval  25414  dchrptlem1  25545  dchrptlem2  25546  lgsdchrval  25635  2lgslem1b  25673  addsq2nreurex  25725  pntpbnd  25869  pntibndlem3  25873  pntibnd  25874  pntlemi  25885  pntleme  25889  pntlemp  25891  pnt3  25893  istrkgld  25950  istrkg3ld  25952  axtgsegcon  25955  axtgpasch  25958  axtgcont1  25959  axtgupdim2  25962  legov  26076  islnopp  26230  ishpg  26250  hpgbr  26251  hpgcom  26258  iscgra1  26301  isinag  26330  isleag  26339  ttgval  26367  ttgitvval  26374  ttgelitv  26375  brbtwn  26391  brcgr  26392  axpasch  26433  axlowdim2  26452  axlowdim  26453  axcontlem2  26457  axcontlem4  26459  axcontlem7  26462  axcontlem8  26463  upgredg2vtx  26632  edglnl  26634  usgredg4  26705  ushgredgedg  26717  ushgredgedgloop  26719  dfnbgr2  26825  nbgrel  26828  nbumgrvtx  26834  nbgrnself  26847  uvtxel1  26884  cusgrfilem2  26944  cusgrfi  26946  vtxd0nedgb  26976  fusgrn0degnn0  26987  wlkonl1iedg  27152  wspniunwspnon  27432  elwwlks2on  27468  clwwlknscsh  27589  erclwwlkneq  27594  eleclclwwlkn  27603  hashecclwwlkn1  27604  umgrhashecclwwlk  27605  3cyclfrgrrn1  27822  friendshipgt3  27958  isgrpo  28054  isgrpoi  28055  grpoidinvlem3  28063  grpoideu  28066  grpoidinv2  28072  nmoofval  28319  nmooval  28320  nmosetn0  28322  nmoolb  28328  nmoubi  28329  nmlno0lem  28350  chcompl  28801  pjhthmo  28863  pjhval  28958  pjpreeq  28959  h1de2ci  29117  elspansn  29127  nmopval  29417  nmopsetn0  29426  nmfnval  29437  nmfnsetn0  29439  eigvecval  29457  hhcno  29465  hhcnf  29466  nmoplb  29468  nmopub  29469  nmfnlb  29485  nmfnleub  29486  eleigvec  29518  nmlnop0iALT  29556  nmopun  29575  nmcexi  29587  branmfn  29666  pjnmopi  29709  cvbr  29843  hatomic  29921  chrelat2  29931  cdjreui  29993  cdj3lem2  29996  elabreximd  30052  br8d  30128  unipreima  30156  abfmpunirn  30162  curry2ima  30199  toslublem  30386  tosglblem  30388  archirng  30483  archiexdiv  30485  archiabllem2a  30489  archiabl  30493  isarchiofld  30569  fedgmul  30656  ccfldextdgrr  30686  crefi  30755  pcmplfin  30768  pstmfval  30780  tpr2rico  30799  rge0scvg  30836  ismntop  30911  esumc  30954  esumpcvgval  30981  esum2dlem  30995  inelsros  31082  diffiunisros  31083  dya2icoseg2  31181  dya2iocuni  31186  eulerpartlemgvv  31279  eulerpartlemgh  31281  hgt749d  31568  tgoldbachgt  31582  bnj66  31779  bnj873  31843  bnj18eq1  31846  bnj1234  31930  bnj1318  31942  subfacp1lem3  32014  pconncn  32056  cnpconn  32062  txpconn  32064  connpconn  32067  iscvm  32091  cvmcov  32095  cvmopnlem  32110  cvmliftlem15  32130  cvmlift3lem2  32152  cvmlift3lem4  32154  cvmlift3  32160  satf  32181  satf0op  32187  sat1el2xp  32189  fmlafvel  32195  fmlasuc  32196  fmla1  32197  br8  32512  br6  32513  br4  32514  dfrdg2  32561  dfrdg3  32562  orderseqlem  32615  poseq  32616  soseq  32617  elno  32674  sltval  32675  noprefixmo  32723  nosupno  32724  nosupdm  32725  nosupfv  32727  nosupres  32728  nosupbnd1lem1  32729  nosupbnd1lem3  32731  nosupbnd1lem4  32732  nosupbnd1lem5  32733  noeta  32743  altxpeq2  32956  funtransport  33013  fvtransport  33014  brcolinear2  33040  colineardim1  33043  segcon2  33087  brsegle  33090  funray  33122  fvray  33123  funline  33124  linedegen  33125  fvline  33126  ellines  33134  nn0prpwlem  33191  fnessref  33226  neibastop2lem  33229  neibastop2  33230  tailfb  33246  unblimceq0lem  33365  unblimceq0  33366  unbdqndv2  33370  bj-finsumval0  34030  relowlssretop  34086  nlpineqsn  34130  pibp19  34136  phpreu  34317  matunitlindflem2  34330  ptrest  34332  poimirlem4  34337  poimirlem17  34350  poimirlem20  34353  poimirlem24  34357  poimirlem26  34359  poimirlem27  34360  poimirlem28  34361  poimirlem31  34364  poimirlem32  34365  poimir  34366  heicant  34368  mblfinlem1  34370  mblfinlem3  34372  mblfinlem4  34373  ismblfin  34374  itg2addnclem  34384  itg2addnclem3  34386  itg2addnc  34387  itg2gt0cn  34388  cnicciblnc  34404  ftc1anclem6  34413  unirep  34430  indexa  34450  sdclem2  34459  sdclem1  34460  sdc  34461  fdc  34462  fdc1  34463  incsequz  34465  istotbnd  34489  sstotbnd2  34494  equivtotbnd  34498  isbnd  34500  bndss  34506  ssbnd  34508  totbndbnd  34509  ismtybndlem  34526  heibor1lem  34529  heiborlem1  34531  heiborlem6  34536  heiborlem8  34538  heiborlem10  34540  heibor  34541  rngoid  34622  isgrpda  34675  isdrngo2  34678  divrngidl  34748  prnc  34787  isfldidl  34788  exanres3  34997  brcoels  35125  br1cossxrnres  35133  eldm1cossres2  35146  prtlem5  35441  prtlem13  35449  prtlem16  35450  islshp  35560  lsmsat  35589  lcvbr  35602  lsatcv0  35612  lshpsmreu  35690  lshpkrlem1  35691  lshpkrlem2  35692  lshpkrlem3  35693  lshpkrcl  35697  lshpset2N  35700  islshpkrN  35701  cvrval  35850  atlex  35897  glbconxN  35959  hlsuprexch  35962  islln  36087  islpln  36111  islpln5  36116  lvolex3N  36119  islvol  36154  islvol5  36160  ispointN  36323  pmapglbx  36350  paddval  36379  elpaddn0  36381  elpaddat  36385  elpadd0  36390  4atex  36657  4atex2  36658  cdlemefrs29bpre1  36978  cdlemefrs32fva  36981  cdlemg33b  37288  dvhb1dimN  37567  dvhopellsm  37698  dib1dim  37746  diclspsn  37775  dihglblem2aN  37874  dihglblem2N  37875  dih1dimatlem  37910  dvh3dimatN  38020  dvh2dim  38026  dvh3dim  38027  dvh4dimN  38028  dvh3dim3N  38030  dochfl1  38057  lcfl7N  38082  lcf1o  38132  lcfrlem39  38162  mapdpglem3  38256  hvmapvalvalN  38342  hdmap14lem2a  38448  hdmapglem7a  38508  3rspcedvd  38548  nnn1suc  38594  prjspeclsp  38669  elrfi  38686  isnacs  38696  nacsfg  38697  nacsfix  38704  mzpcompact2lem  38743  eldiophb  38749  eldioph  38750  eldioph2  38754  eldioph2b  38755  eldioph3  38758  eldiophss  38767  diophrex  38768  sbcrexgOLD  38778  sbc2rexgOLD  38781  rexrabdioph  38787  rexfrabdioph  38788  elnn0rabdioph  38796  dvdsrabdioph  38803  eldioph4b  38804  eldioph4i  38805  diophren  38806  rencldnfilem  38813  pell1234qrdich  38854  jm2.27  39001  expdiophlem1  39014  wepwsolem  39038  aomclem8  39057  islnr3  39111  lnr2i  39112  lpirlnr  39113  hbtlem1  39119  hbtlem2  39120  hbtlem7  39121  hbtlem4  39122  hbtlem5  39124  hbtlem6  39125  dgraaval  39140  dgraalem  39141  dgraaub  39144  rngunsnply  39169  brtrclfv2  39435  clsk1indlem1  39758  extoimad  39879  mnuop123d  39973  mnuop23d  39977  mnuprdlem1  39983  mnuprdlem2  39984  elabrexg  40722  foelrnf  40872  disjrnmpt2  40874  upbdrech  41002  ssfiunibd  41006  supxrgere  41031  supxrgelem  41035  supxrge  41036  suplesup  41037  infxr  41065  infleinf  41070  supxrunb3  41103  unb2ltle  41121  uzub  41137  supminfxr  41172  iccshift  41226  iooshift  41230  climinf  41319  climinff  41324  ellimcabssub0  41330  climf  41335  limcperiod  41341  limclner  41364  climf2  41379  clim2d  41386  limsupref  41398  limsuppnfd  41415  limsuppnf  41424  climinfmpt  41428  limsupubuzmpt  41432  limsupmnf  41434  limsupre2lem  41437  limsupre2  41438  limsupmnfuz  41440  limsupre2mpt  41443  limsupre3lem  41445  limsupre3  41446  limsupre3mpt  41447  limsupre3uzlem  41448  limsupre3uz  41449  limsupreuz  41450  limsupreuzmpt  41452  climuz  41457  liminfreuzlem  41515  liminfreuz  41516  xlimmnfvlem1  41545  xlimmnfv  41547  xlimpnfvlem1  41549  xlimpnfv  41551  cncfshiftioo  41606  fperdvper  41634  itgiccshift  41696  itgperiod  41697  stoweidlem27  41744  stoweidlem31  41748  stoweidlem43  41760  stoweidlem46  41763  stoweidlem52  41769  stoweidlem60  41777  fourierdlem42  41866  fourierdlem48  41871  fourierdlem51  41874  fourierdlem54  41877  fourierdlem63  41886  fourierdlem64  41887  fourierdlem65  41888  fourierdlem68  41891  fourierdlem70  41893  fourierdlem71  41894  fourierdlem73  41896  fourierdlem80  41903  fourierdlem81  41904  fourierdlem89  41912  fourierdlem90  41913  fourierdlem91  41914  fourierdlem92  41915  fourierdlem96  41919  fourierdlem97  41920  fourierdlem98  41921  fourierdlem99  41922  fourierdlem100  41923  fourierdlem103  41926  fourierdlem104  41927  fourierdlem105  41928  fourierdlem108  41931  fourierdlem109  41932  fourierdlem110  41933  fourierdlem112  41935  fourierdlem113  41936  sge0pnffigt  42110  sge0resplit  42120  ovnval2  42259  ovnval2b  42266  ovnlecvr  42272  ovnpnfelsup  42273  ovn0lem  42279  ovnsubaddlem1  42284  hoidmvlelem1  42309  ovnhoilem1  42315  ovnhoi  42317  ovnlecvr2  42324  hoiqssbl  42339  ovolval5lem2  42367  ovolval5lem3  42368  ovolval5  42369  ovnovol  42373  smfsuplem2  42518  smfsup  42520  smfinflem  42523  smfinf  42524  cbvrex2  42709  2reu8i  42719  2reuimp0  42720  afvelrnb  42769  afvelrnb0  42770  iccelpart  42966  iccpartiun  42967  icceuelpart  42969  sprsymrelf1lem  43022  sprsymrelf  43026  fmtnofac2lem  43099  fmtnofac2  43100  fmtnofac1  43101  m1expevenALTV  43181  odd2np1ALTV  43208  opoeALTV  43217  opeoALTV  43218  mogoldbblem  43254  nfermltlrev  43278  isgbow  43286  isgbo  43287  7gbow  43306  9gbo  43308  11gbo  43309  sbgoldbwt  43311  mogoldbb  43319  sbgoldbo  43321  nnsum3primesgbe  43326  nnsum4primesodd  43330  nnsum4primesoddALTV  43331  bgoldbtbnd  43343  uspgrsprf1  43391  uspgrsprfo  43392  0nodd  43446  1odd  43447  2nodd  43448  0even  43567  1neven  43568  2even  43569  2zlidl  43570  2zrngamgm  43575  2zrngagrp  43579  2zrngmmgm  43582  2zrngnmrid  43586  lcoval  43835  el0ldep  43889  ldepspr  43896  zlmodzxzldep  43927  line  44088  rrxline  44090