Theorem rexbidv 2946

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

Hypothesis

Ref	Expression
rexbidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
rexbidv	|- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)

Proof of Theorem rexbidv

Step	Hyp	Ref	Expression
1		rexbidv.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	adantr 466	. 2 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
3	2	rexbidva 2943	1 |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 187   e. wcel 1870   E.wrex 2783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-rex 2788

This theorem is referenced by:  rexbiiOLD  2948  2rexbidv  2953  rexralbidv  2954  rexeqbi1dv  3041  rexeqbidv  3047  cbvrex2v  3071  rspc2ev  3199  rspc3ev  3201  ceqsrex2v  3213  uniiunlem  3555  rabasiun  4306  eliun  4307  dfiin2g  4335  dfiunv2  4338  elrnmpt  5101  elrnmptg  5104  elimag  5192  fvelrnb  5928  fvelimab  5937  foelrn  6056  foco2  6057  elabrex  6163  abrexco  6164  f1oiso  6257  f1oiso2  6258  grprinvlem  6521  orduninsuc  6684  funcnvuni  6760  fun11iun  6767  abrexex2g  6784  abrexex2  6788  f1oweALT  6791  el2xptp  6850  tfrlem12  7115  seqomlem2  7176  nneob  7361  qseq2  7422  elqsg  7423  elixpsn  7569  ixpsnf1o  7570  isfi  7600  enfi  7794  pssnn  7796  frfi  7822  unblem1  7829  unblem2  7830  unbnn2  7834  fofinf1o  7858  finsschain  7887  indexfi  7888  elfi  7933  marypha1lem  7953  supeq3  7969  supmo  7972  suplub  7980  supisolem  7995  eqinf  8006  infval  8008  infglb  8012  infglbb  8013  oieq1  8027  ordtypelem2  8034  ordtypelem3  8035  ordtypelem9  8041  wemaplem1  8061  brwdom2  8088  brwdom3  8097  unwdomg  8099  oemapval  8187  cantnf  8197  wemapwe  8201  cnfcom3clem  8209  tz9.13  8261  tz9.13g  8262  cardf2  8376  isnum2  8378  ennum  8380  cardiun  8415  infxpenc2  8451  aceq1  8546  aceq2  8548  dfac5lem3  8554  dfac5lem4  8555  dfac2a  8558  dfac2  8559  kmlem9  8586  kmlem12  8589  kmlem14  8591  ackbij1  8666  cflm  8678  cfss  8693  cofsmo  8697  cfsmolem  8698  cfcoflem  8700  coftr  8701  isfin7  8729  fin23lem26  8753  isf32lem5  8785  fin1a2lem11  8838  hsmexlem2  8855  axdc3lem3  8880  axdc3  8882  numthcor  8922  zorn2lem7  8930  brdom3  8954  brdom7disj  8957  brdom6disj  8958  iundom2g  8963  fpwwe2  9067  winainflem  9117  winalim2  9120  inar1  9199  tskuni  9207  nqereu  9353  prnmax  9419  genpv  9423  genpnmax  9431  genpass  9433  prlem936  9471  recexsrlem  9526  map2psrpr  9533  supsrlem  9534  axrrecex  9586  axpre-sup  9592  dedekind  9796  cnegex  9813  recex  10243  fimaxre3  10553  infm3  10568  supaddc  10574  supadd  10575  supmul1  10576  supmullem1  10577  supmullem2  10578  supmul  10579  creur  10603  creui  10604  cju  10605  nnunb  10865  arch  10866  xrsupsslem  11592  xrinfmsslem  11593  xrsupss  11594  xrinfmss  11595  xrub  11597  supxrunb1  11605  supxrunb2  11606  infmxrgelbOLD  11625  infmremnf  11633  infmrp1  11634  fsequb2  12186  iswrd  12659  iswrdOLD  12660  wrdval  12661  csbwrdg  12683  cshword  12878  0csh0  12880  2cshwcshw  12909  scshwfzeqfzo  12910  shftfval  13112  abs1m  13377  rexfiuz  13389  limsupbnd2  13524  limsupbnd2OLD  13525  clim  13536  rlim  13537  rlim2  13538  rlim0  13550  rlim0lt  13551  ello1mpt2  13564  o1lo1  13579  o1compt  13629  rlimdiv  13687  climsup  13711  sumeq1  13733  sumeq2w  13736  summo  13761  fsum  13764  fsumcvg3  13773  infcvgaux2i  13894  mertenslem1  13918  mertenslem2  13919  mertens  13920  prodeq1f  13940  prodeq2w  13944  prodmo  13968  fprod  13973  divides  14285  odd2np1lem  14342  divalglem4  14352  divalglem10  14358  divalg  14359  gcdcllem3  14449  bezoutlem1  14477  exprmfct  14610  nnnn0modprm0  14711  opeo  14717  omeo  14718  pythagtriplem2  14721  pythagtrip  14738  pceu  14750  pcprmpw2  14785  unbenlem  14806  4sqlem12  14854  vdwapval  14877  vdwapun  14878  vdwmc2  14883  vdwpc  14884  vdwlem2  14886  vdwlem10  14894  vdwlem13  14897  vdwnnlem1  14899  rami  14926  cshwsiun  15024  cshwrepswhash1  15027  brssc  15661  isdrs  16121  drsdir  16122  drsdirfi  16125  isdrs2  16126  ipodrsima  16353  gsumvalx  16455  gsumpropd  16457  gsumress  16461  isnsgrp  16473  sgrp2nmndlem5  16605  grpinvex  16623  grp1  16700  imasgrp2  16743  conjnmzb  16859  gaorb  16903  orbsta  16909  symgfix2  16999  symgextfo  17005  pmtrprfvalrn  17071  psgnunilem3  17079  psgneu  17089  psgnval  17090  psgnvali  17091  psgnvalii  17092  ispgp  17170  subgpgp  17175  sylow1  17181  pgpfi  17183  sylow2blem3  17200  fislw  17203  sylow3lem2  17206  lsmelvalm  17229  lsmass  17246  pj1fval  17270  pj1val  17271  pj1eu  17272  pj1id  17275  efgrelexlema  17325  efgrelexlemb  17326  efgredeu  17328  cyggeninv  17444  cygabl  17451  pgpfac1lem2  17634  pgpfac1lem3  17636  pgpfac1lem4  17637  pgpfac1  17639  pgpfaclem2  17641  pgpfac  17643  dvdsrval  17799  dvdsr  17800  subrgdvds  17948  lss1d  18112  lspsn  18151  lspsnel  18152  lspsolvlem  18291  rspsn  18404  opsrval  18624  znf1o  19044  cygznlem3  19062  psgndiflemA  19091  ellspd  19282  mat1dimelbas  19418  mat1dimbas  19419  scmatval  19451  scmatel  19452  scmateALT  19459  mat0scmat  19485  decpmataa0  19714  decpmatmulsumfsupp  19719  pmatcollpw2lem  19723  pm2mpmhmlem1  19764  chpscmat  19788  basis2  19888  eltg2  19895  tg2  19902  isclo  20025  neival  20040  isnei  20041  isneip  20043  restbas  20096  neitr  20118  cnpval  20174  iscnp  20175  cnpimaex  20194  lmbr  20196  lmbr2  20197  cnprest2  20228  lmff  20239  regsep  20272  pnrmopn  20281  nrmsep3  20293  isnrm2  20296  iscmp  20325  cmpsublem  20336  cmpsub  20337  tgcmp  20338  sscmp  20342  hauscmplem  20343  1stcclb  20381  1stcfb  20382  is2ndc  20383  2ndc1stc  20388  1stcrest  20390  2ndcctbss  20392  1stcelcls  20398  llyeq  20407  nllyeq  20408  hausllycmp  20431  lly1stc  20433  refssex  20448  refun0  20452  islocfin  20454  locfinnei  20460  comppfsc  20469  txbas  20504  ptval  20507  ptpjopn  20549  ptclsg  20552  txcnp  20557  ptcnp  20559  txrest  20568  ptrescn  20576  txcmp  20580  tx1stc  20587  xkococn  20597  kqreglem1  20678  fbasssin  20773  fbssfi  20774  fbssint  20775  fbun  20777  fgss2  20811  fgcl  20815  ufli  20851  fmfnfmlem3  20893  fbflim2  20914  hauspwpwf1  20924  flfneii  20929  flftg  20933  txflf  20943  fclscf  20962  alexsubb  20983  alexsubALT  20988  tsmssubm  21079  ustincl  21144  ustdiag  21145  ustinvel  21146  ustexhalf  21147  ust0  21156  trust  21166  elutop  21170  ucnval  21214  ucncn  21222  cfiluexsm  21227  cfiluweak  21232  blssps  21361  blss  21362  imasf1oxms  21426  mopni  21429  metss  21445  metrest  21461  metcnp3  21477  cfilucfil  21496  metuel2  21502  nlmvscn  21612  nrginvrcn  21616  icccmplem1  21742  icccmplem2  21743  icccmp  21745  divcn  21787  cncfval  21807  elcncf2  21809  cncfmet  21827  cnheibor  21870  evth  21874  lebnumlem3  21878  lebnum  21879  xlebnum  21880  lebnumii  21881  ipcn  22101  lmmbr  22112  lmmbr2  22113  cfilfval  22118  cfili  22122  iscfil3  22127  caufval  22129  iscau  22130  iscau2  22131  equivcfil  22153  equivcau  22154  lmcau  22166  ovolval  22296  elovolm  22297  ovolgelb  22302  ovoliunlem1  22324  ovoliun2  22328  ovolshftlem1  22331  ovolscalem1  22335  ovolicc  22345  ioombl1lem4  22382  uniioombllem2  22408  uniioombllem2OLD  22409  mbfaddlem  22484  mbfsup  22488  mbfinf  22489  mbfinfOLD  22490  mbflimsup  22491  mbflimsupOLD  22492  i1fmulc  22529  itg1climres  22540  itg2val  22554  itg2l  22555  itg2leub  22560  itg2seq  22568  itg2monolem1  22576  itg2mono  22579  itg2i1fseq2  22582  cniccibl  22666  ellimc3  22702  limciun  22717  dvferm1  22805  dvferm2  22807  lhop1lem  22833  ply1divex  22953  ig1peu  22988  plyval  23006  elply2  23009  coeval  23036  coeeu  23038  coelem  23039  coeeq  23040  plydivlem4  23108  plydivex  23109  aannenlem2  23141  aalioulem2  23145  aaliou2  23152  ulmval  23191  ulm2  23196  ulmcau  23206  ulmdvlem3  23213  abelthlem9  23251  abelth  23252  efif1olem4  23350  eflogeq  23407  efopn  23459  cxpcn3  23544  cxpeq  23553  rlimcnp  23747  lgamgulmlem6  23815  muval  23913  dchrptlem1  24046  dchrptlem2  24047  lgsdchrval  24129  pntpbnd  24280  pntibndlem3  24284  pntibnd  24285  pntlemi  24296  pntleme  24300  pntlemp  24302  pnt3  24304  istrkgld  24361  istrkg3ld  24363  axtgsegcon  24366  axtgpasch  24369  axtgcont1  24370  axtgupdim2  24373  legov  24481  islnopp  24629  ishpg  24648  hpgbr  24649  hpgcom  24656  iscgra  24698  iscgra1  24699  isinag  24723  ttgval  24742  ttgitvval  24749  ttgelitv  24750  brbtwn  24766  brcgr  24767  axpasch  24808  axlowdim2  24827  axlowdim  24828  axcontlem2  24832  axcontlem4  24834  axcontlem7  24837  axcontlem8  24838  nbgraf1olem1  25005  cusgrafilem2  25044  cusgrafi  25046  wwlkn0  25253  clwwlknscsh  25383  erclwwlkneq  25387  eclclwwlkn0  25395  eleclclwwlkn  25397  hashecclwwlkn1  25398  usghashecclwwlk  25399  el2wlksot  25444  el2pthsot  25445  2spot2iun2spont  25455  iseupa  25529  3cyclfrgrarn1  25576  usgn0fidegnn0  25593  frgrancvvdeqlem4  25597  friendshipgt3  25685  isgrpo  25760  isgrpoi  25762  grpoidinvlem3  25770  grpoideu  25773  grpoidinv2  25782  isgrp2d  25799  isgrpda  25861  ghgrpOLD  25932  rngoid  25947  nmoofval  26239  nmooval  26240  nmosetn0  26242  nmoolb  26248  nmoubi  26249  nmlno0lem  26270  chcompl  26721  pjhthmo  26781  pjhval  26876  pjpreeq  26877  h1de2ci  27035  elspansn  27045  nmopval  27335  nmopsetn0  27344  nmfnval  27355  nmfnsetn0  27357  eigvecval  27375  hhcno  27383  hhcnf  27384  nmoplb  27386  nmopub  27387  nmfnlb  27403  nmfnleub  27404  eleigvec  27436  nmlnop0iALT  27474  nmopun  27493  nmcexi  27505  branmfn  27584  pjnmopi  27627  cvbr  27761  hatomic  27839  chrelat2  27849  cdjreui  27911  cdj3lem2  27914  reuxfr4d  27952  elabreximd  27971  br8d  28048  unipreima  28076  abfmpunirn  28082  curry2ima  28120  infxrge0glb  28177  toslublem  28257  tosglblem  28259  archirng  28334  archiexdiv  28336  archiabllem2a  28340  archiabl  28344  isarchiofld  28410  crefi  28504  pcmplfin  28517  pstmfval  28529  tpr2rico  28548  rge0scvg  28585  ismntop  28660  esumc  28702  esumpcvgval  28729  esum2dlem  28743  inelsros  28830  diffiunisros  28831  dya2icoseg2  28930  dya2iocuni  28935  eulerpartlemgvv  29026  eulerpartlemgh  29028  bnj66  29450  bnj873  29514  bnj18eq1  29517  bnj1234  29601  bnj1318  29613  subfacp1lem3  29684  pconcn  29726  cnpcon  29732  txpcon  29734  conpcon  29737  iscvm  29761  cvmcov  29765  cvmopnlem  29780  cvmliftlem15  29800  cvmlift3lem2  29822  cvmlift3lem4  29824  cvmlift3  29830  br8  30174  br6  30175  br4  30176  dfrdg2  30220  dfrdg3  30221  orderseqlem  30268  poseq  30269  soseq  30270  elno  30311  sltval  30312  nobndlem6  30362  nofulllem1  30367  nofulllem2  30368  nofulllem5  30371  altxpeq2  30517  funtransport  30574  fvtransport  30575  brcolinear2  30601  colineardim1  30604  segcon2  30648  brsegle  30651  funray  30683  fvray  30684  funline  30685  linedegen  30686  fvline  30687  ellines  30695  gtinf  30751  nn0prpwlem  30754  fnessref  30789  neibastop2lem  30792  neibastop2  30793  tailfb  30809  bj-finsumval0  31438  relowlssretop  31491  phpreu  31623  ptrest  31633  poimirlem4  31638  poimirlem17  31651  poimirlem20  31654  poimirlem24  31658  poimirlem26  31660  poimirlem27  31661  poimirlem28  31662  poimirlem31  31665  poimirlem32  31666  poimir  31667  heicant  31669  mblfinlem1  31671  mblfinlem3  31673  mblfinlem4  31674  ismblfin  31675  itg2addnclem  31687  itg2addnclem3  31689  itg2addnc  31690  itg2gt0cn  31691  cnicciblnc  31707  ftc1anclem6  31716  unirep  31733  indexa  31754  sdclem2  31765  sdclem1  31766  sdc  31767  fdc  31768  fdc1  31769  incsequz  31771  istotbnd  31795  sstotbnd2  31800  equivtotbnd  31804  isbnd  31806  bndss  31812  ssbnd  31814  totbndbnd  31815  ismtybndlem  31832  heibor1lem  31835  heiborlem1  31837  heiborlem6  31842  heiborlem8  31844  heiborlem10  31846  heibor  31847  isdrngo2  31891  divrngidl  31955  prnc  31994  isfldidl  31995  prtlem5  32126  prtlem13  32138  prtlem16  32139  islshp  32244  lsmsat  32273  lcvbr  32286  lsatcv0  32296  lshpsmreu  32374  lshpkrlem1  32375  lshpkrlem2  32376  lshpkrlem3  32377  lshpkrcl  32381  lshpset2N  32384  islshpkrN  32385  cvrval  32534  atlex  32581  glbconxN  32642  hlsuprexch  32645  islln  32770  islpln  32794  islpln5  32799  lvolex3N  32802  islvol  32837  islvol5  32843  ispointN  33006  pmapglbx  33033  paddval  33062  elpaddn0  33064  elpaddat  33068  elpadd0  33073  4atex  33340  4atex2  33341  cdlemefrs29bpre1  33663  cdlemefrs32fva  33666  cdlemg33b  33973  dvhb1dimN  34252  dvhopellsm  34384  dib1dim  34432  diclspsn  34461  dihglblem2aN  34560  dihglblem2N  34561  dih1dimatlem  34596  dvh3dimatN  34706  dvh2dim  34712  dvh3dim  34713  dvh4dimN  34714  dvh3dim3N  34716  dochfl1  34743  lcfl7N  34768  lcf1o  34818  lcfrlem39  34848  mapdpglem3  34942  hvmapvalvalN  35028  hdmap14lem2a  35137  hdmapglem7a  35197  elrfi  35235  isnacs  35245  nacsfg  35246  nacsfix  35253  mzpcompact2lem  35292  eldiophb  35298  eldioph  35299  eldioph2  35303  eldioph2b  35304  eldioph3  35307  eldiophss  35316  diophrex  35317  sbcrexgOLD  35327  sbc2rexgOLD  35330  rexrabdioph  35336  rexfrabdioph  35337  elnn0rabdioph  35345  dvdsrabdioph  35352  eldioph4b  35353  eldioph4i  35354  diophren  35355  rencldnfilem  35362  pell1234qrdich  35405  jm2.27  35559  expdiophlem1  35572  wepwsolem  35596  aomclem8  35615  islnr3  35670  lnr2i  35671  lpirlnr  35672  hbtlem1  35678  hbtlem2  35679  hbtlem7  35680  hbtlem4  35681  hbtlem5  35683  hbtlem6  35684  dgraaval  35699  dgraalem  35700  dgraaub  35703  rngunsnply  35728  brtrclfv2  35948  extoimad  36234  elabrexg  37000  foelrnf  37074  disjrnmpt2  37076  upbdrech  37122  ssfiunibd  37126  supxrgere  37155  supxrgelem  37159  supxrge  37160  suplesup  37161  iccshift  37194  iooshift  37198  infrglbOLD  37231  climinf  37246  climinfOLD  37247  climinff  37252  climinffOLD  37253  ellimcabssub0  37259  climf  37264  limcperiod  37270  limclner  37294  cncfshiftioo  37332  fperdvper  37352  itgiccshift  37416  itgperiod  37417  stoweidlem27  37446  stoweidlem31  37451  stoweidlem43  37463  stoweidlem46  37466  stoweidlem52  37472  stoweidlem60  37480  fourierdlem42  37570  fourierdlem48  37576  fourierdlem51  37579  fourierdlem54  37582  fourierdlem63  37591  fourierdlem64  37592  fourierdlem65  37593  fourierdlem68  37596  fourierdlem70  37598  fourierdlem71  37599  fourierdlem73  37601  fourierdlem80  37608  fourierdlem81  37609  fourierdlem89  37617  fourierdlem90  37618  fourierdlem91  37619  fourierdlem92  37620  fourierdlem96  37624  fourierdlem97  37625  fourierdlem98  37626  fourierdlem99  37627  fourierdlem100  37628  fourierdlem103  37631  fourierdlem104  37632  fourierdlem105  37633  fourierdlem108  37636  fourierdlem109  37637  fourierdlem110  37638  fourierdlem112  37640  fourierdlem113  37641  sge0pnffigt  37762  sge0resplit  37772  cbvrex2  37975  afvelrnb  38045  afvelrnb0  38046  iccelpart  38127  iccpartiun  38128  icceuelpart  38130  m1expevenALTV  38157  odd2np1ALTV  38183  opoeALTV  38192  opeoALTV  38193  isgbo  38233  isgboa  38234  7gbo  38253  9gboa  38255  11gboa  38256  bgoldbwt  38258  nnsum3primesgbe  38267  nnsum4primesodd  38271  nnsum4primesoddALTV  38272  bgoldbtbnd  38284  cshword2  38358  0nodd  38558  1odd  38559  2nodd  38560  0even  38679  1neven  38680  2even  38681  2zlidl  38682  2zrngamgm  38687  2zrngagrp  38691  2zrngmmgm  38694  2zrngnmrid  38698  lcoval  38955  el0ldep  39009  ldepspr  39016  zlmodzxzldep  39047