Theorem rexbidv 2731

Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.)

Hypothesis

Ref	Expression
ralbidv.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		nfv 1673	. 2 |- F/ x ph
2		ralbidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	rexbid 2729	1 |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 184   E.wrex 2711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-rex 2716

This theorem is referenced by:  rexbii  2735  2rexbidv  2753  rexralbidv  2754  rexeqbi1dv  2921  rexeqbidv  2927  cbvrex2v  2951  rspc2ev  3076  rspc3ev  3078  ceqsrex2v  3090  sbcrexgOLD  3267  uniiunlem  3435  eliun  4170  dfiin2g  4198  dfiunv2  4201  elrnmpt  5081  elrnmptg  5084  elimag  5168  fvelrnb  5734  fvelimab  5742  foelrn  5857  foco2  5858  elabrex  5955  abrexco  5956  f1oiso  6037  f1oiso2  6038  grprinvlem  6296  orduninsuc  6449  funcnvuni  6525  fun11iun  6532  abrexex2g  6549  abrexex2  6553  f1oweALT  6556  recseq  6825  tfrlem12  6840  seqomlem2  6898  nneob  7083  qseq2  7143  elqsg  7144  elixpsn  7294  ixpsnf1o  7295  isfi  7325  enfi  7521  pssnn  7523  frfi  7549  unblem1  7556  unblem2  7557  unbnn2  7561  fofinf1o  7584  finsschain  7610  indexfi  7611  elfi  7655  marypha1lem  7675  supeq3  7691  supmo  7694  suplub  7702  supisolem  7712  oieq1  7718  ordtypelem2  7725  ordtypelem3  7726  ordtypelem9  7732  wemaplem1  7752  brwdom2  7780  brwdom3  7789  unwdomg  7791  oemapval  7883  cantnf  7893  cantnfOLD  7915  wemapwe  7920  wemapweOLD  7921  cnfcom3clem  7930  cnfcom3clemOLD  7938  tz9.13  7990  tz9.13g  7991  cardf2  8105  isnum2  8107  ennum  8109  cardiun  8144  infxpenc2  8180  infxpenc2OLD  8184  aceq1  8279  aceq2  8281  dfac5lem3  8287  dfac5lem4  8288  dfac2a  8291  dfac2  8292  kmlem9  8319  kmlem12  8322  kmlem14  8324  ackbij1  8399  cflm  8411  cfss  8426  cofsmo  8430  cfsmolem  8431  cfcoflem  8433  coftr  8434  isfin7  8462  fin23lem26  8486  isf32lem5  8518  fin1a2lem11  8571  hsmexlem2  8588  axdc3lem3  8613  axdc3  8615  numthcor  8655  zorn2lem7  8663  brdom3  8687  brdom7disj  8690  brdom6disj  8691  iundom2g  8696  fpwwe2  8802  winainflem  8852  winalim2  8855  inar1  8934  tskuni  8942  nqereu  9090  prnmax  9156  genpv  9160  genpnmax  9168  genpass  9170  prlem936  9208  recexsrlem  9262  map2psrpr  9269  supsrlem  9270  axrrecex  9322  axpre-sup  9328  dedekind  9525  cnegex  9542  recex  9960  fimaxre3  10271  infm3  10281  supmul1  10287  supmullem1  10288  supmullem2  10289  supmul  10290  creur  10308  creui  10309  cju  10310  nnunb  10567  arch  10568  xrsupsslem  11261  xrinfmsslem  11262  xrsupss  11263  xrinfmss  11264  xrub  11266  supxrunb1  11274  supxrunb2  11275  infmxrgelb  11289  fsequb2  11790  iswrd  12229  wrdval  12230  csbwrdg  12249  cshword  12420  0csh0  12422  shftfval  12551  abs1m  12815  rexfiuz  12827  limsupbnd2  12953  clim  12964  rlim  12965  rlim2  12966  rlim0  12978  rlim0lt  12979  ello1mpt2  12992  o1lo1  13007  o1compt  13057  rlimdiv  13115  climsup  13139  sumeq1  13158  sumeq2w  13161  summo  13186  fsum  13189  fsumcvg3  13198  infcvgaux2i  13312  mertenslem1  13336  mertenslem2  13337  mertens  13338  divides  13529  odd2np1lem  13583  divalglem4  13592  divalglem10  13598  divalg  13599  gcdcllem3  13689  bezoutlem1  13714  exprmfct  13788  nnnn0modprm0  13866  opeo  13872  omeo  13873  pythagtriplem2  13876  pythagtrip  13893  pceu  13905  pcprmpw2  13940  unbenlem  13961  4sqlem12  14009  vdwapval  14026  vdwapun  14027  vdwmc2  14032  vdwpc  14033  vdwlem2  14035  vdwlem10  14043  vdwlem13  14046  vdwnnlem1  14048  rami  14068  cshwsiun  14118  cshwrepswhash1  14121  brssc  14719  isdrs  15096  drsdir  15097  drsdirfi  15100  isdrs2  15101  ipodrsima  15327  gsumvalx  15493  gsumpropd  15495  gsumress  15498  grpinvex  15544  imasgrp2  15661  conjnmzb  15772  gaorb  15816  orbsta  15822  symgfix2  15912  symgextfo  15918  pmtrprfvalrn  15985  psgnunilem3  15993  psgneu  16003  psgnval  16004  psgnvali  16005  psgnvalii  16006  ispgp  16082  subgpgp  16087  sylow1  16093  pgpfi  16095  sylow2blem3  16112  fislw  16115  sylow3lem2  16118  lsmelvalm  16141  lsmass  16158  pj1fval  16182  pj1val  16183  pj1eu  16184  pj1id  16187  efgrelexlema  16237  efgrelexlemb  16238  efgredeu  16240  cyggeninv  16351  cygabl  16358  pgpfac1lem2  16564  pgpfac1lem3  16566  pgpfac1lem4  16567  pgpfac1  16569  pgpfaclem2  16571  pgpfac  16573  dvdsrval  16725  dvdsr  16726  subrgdvds  16857  lss1d  17021  lspsn  17060  lspsnel  17061  lspsolvlem  17200  rspsn  17313  opsrval  17531  znf1o  17959  cygznlem3  17977  psgndiflemA  18006  ellspd  18205  ellspdOLD  18206  basis2  18531  eltg2  18538  tg2  18545  isclo  18666  neival  18681  isnei  18682  isneip  18684  restbas  18737  neitr  18759  cnpval  18815  iscnp  18816  cnpimaex  18835  lmbr  18837  lmbr2  18838  cnprest2  18869  lmff  18880  regsep  18913  pnrmopn  18922  nrmsep3  18934  isnrm2  18937  iscmp  18966  cmpsublem  18977  cmpsub  18978  tgcmp  18979  sscmp  18983  hauscmplem  18984  1stcclb  19023  1stcfb  19024  is2ndc  19025  2ndc1stc  19030  1stcrest  19032  2ndcctbss  19034  1stcelcls  19040  llyeq  19049  nllyeq  19050  hausllycmp  19073  lly1stc  19075  txbas  19115  ptval  19118  ptpjopn  19160  ptclsg  19163  txcnp  19168  ptcnp  19170  txrest  19179  ptrescn  19187  txcmp  19191  tx1stc  19198  xkococn  19208  kqreglem1  19289  fbasssin  19384  fbssfi  19385  fbssint  19386  fbun  19388  fgss2  19422  fgcl  19426  ufli  19462  fmfnfmlem3  19504  fbflim2  19525  hauspwpwf1  19535  flfneii  19540  flftg  19544  txflf  19554  fclscf  19573  alexsubb  19593  alexsubALT  19598  tsmssubm  19691  ustincl  19757  ustdiag  19758  ustinvel  19759  ustexhalf  19760  ust0  19769  trust  19779  elutop  19783  ucnval  19827  ucncn  19835  cfiluexsm  19840  cfiluweak  19845  blssps  19974  blss  19975  imasf1oxms  20039  mopni  20042  metss  20058  metrest  20074  metcnp3  20090  cfilucfilOLD  20119  cfilucfil  20120  metuel2  20129  nlmvscn  20243  nrginvrcn  20247  icccmplem1  20374  icccmplem2  20375  icccmp  20377  divcn  20419  cncfval  20439  elcncf2  20441  cncfmet  20459  cnheibor  20502  evth  20506  lebnumlem3  20510  lebnum  20511  xlebnum  20512  lebnumii  20513  ipcn  20733  lmmbr  20744  lmmbr2  20745  cfilfval  20750  cfili  20754  iscfil3  20759  caufval  20761  iscau  20762  iscau2  20763  equivcfil  20785  equivcau  20786  lmcau  20798  ovolval  20932  elovolm  20933  ovolgelb  20938  ovoliunlem1  20960  ovoliun2  20964  ovolshftlem1  20967  ovolscalem1  20971  ovolicc  20981  ioombl1lem4  21017  uniioombllem2  21038  mbfaddlem  21113  mbfsup  21117  mbfinf  21118  mbflimsup  21119  i1fmulc  21156  itg1climres  21167  itg2val  21181  itg2l  21182  itg2leub  21187  itg2seq  21195  itg2monolem1  21203  itg2mono  21206  itg2i1fseq2  21209  cniccibl  21293  ellimc3  21329  limciun  21344  dvferm1  21432  dvferm2  21434  lhop1lem  21460  ply1divex  21583  ig1peu  21618  plyval  21636  elply2  21639  coeval  21666  coeeu  21668  coelem  21669  coeeq  21670  plydivlem4  21737  plydivex  21738  aannenlem2  21770  aalioulem2  21774  aaliou2  21781  ulmval  21820  ulm2  21825  ulmcau  21835  ulmdvlem3  21842  abelthlem9  21880  abelth  21881  efif1olem4  21976  eflogeq  22025  efopn  22078  cxpcn3  22161  cxpeq  22170  rlimcnp  22334  muval  22445  dchrptlem1  22578  dchrptlem2  22579  lgsdchrval  22661  pntpbnd  22812  pntibndlem3  22816  pntibnd  22817  pntlemi  22828  pntleme  22832  pntlemp  22834  pnt3  22836  axtgsegcon  22900  axtgpasch  22903  axtgcont1  22904  legov  22987  ttgval  23072  ttgitvval  23079  ttgelitv  23080  brbtwn  23096  brcgr  23097  axpasch  23138  axlowdim2  23157  axlowdim  23158  axcontlem2  23162  axcontlem4  23164  axcontlem7  23167  axcontlem8  23168  nbgraf1olem1  23301  cusgrafilem2  23339  cusgrafi  23341  iseupa  23537  isgrpo  23634  isgrpoi  23636  grpoidinvlem3  23644  grpoideu  23647  grpoidinv2  23656  isgrp2d  23673  isgrpda  23735  ghgrp  23806  rngoid  23821  nmoofval  24113  nmooval  24114  nmosetn0  24116  nmoolb  24122  nmoubi  24123  nmlno0lem  24144  chcompl  24596  pjhthmo  24656  pjhval  24751  pjpreeq  24752  h1de2ci  24910  elspansn  24920  nmopval  25211  nmopsetn0  25220  nmfnval  25231  nmfnsetn0  25233  eigvecval  25251  hhcno  25259  hhcnf  25260  nmoplb  25262  nmopub  25263  nmfnlb  25279  nmfnleub  25280  eleigvec  25312  nmlnop0iALT  25350  nmopun  25369  nmcexi  25381  branmfn  25460  pjnmopi  25503  cvbr  25637  hatomic  25715  chrelat2  25725  cdjreui  25787  cdj3lem2  25790  reuxfr4d  25825  elabreximd  25842  br8d  25893  unipreima  25912  abfmpunirn  25918  curry2ima  25954  toslublem  26079  tosglblem  26081  archirng  26156  archiexdiv  26158  archiabllem2a  26162  archiabl  26166  isarchiofld  26236  pstmfval  26275  tpr2rico  26294  rge0scvg  26331  esumc  26457  esumpcvgval  26479  dya2icoseg2  26645  dya2iocuni  26650  eulerpartlemgvv  26711  eulerpartlemgh  26713  lgamgulmlem6  26972  subfacp1lem3  27022  pconcn  27065  cnpcon  27071  txpcon  27073  conpcon  27076  iscvm  27100  cvmcov  27104  cvmopnlem  27119  cvmliftlem15  27139  cvmlift3lem2  27161  cvmlift3lem4  27163  cvmlift3  27169  prodeq1f  27372  prodeq2w  27376  prodmo  27400  fprod  27405  br8  27517  br6  27518  br4  27519  dfrdg2  27560  dfrdg3  27561  orderseqlem  27664  poseq  27665  soseq  27666  elno  27738  sltval  27739  nobndlem6  27789  nofulllem1  27794  nofulllem2  27795  nofulllem5  27798  altxpeq2  27956  funtransport  28013  fvtransport  28014  brcolinear2  28040  colineardim1  28043  segcon2  28087  brsegle  28090  funray  28122  fvray  28123  funline  28124  linedegen  28125  fvline  28126  ellines  28134  supaddc  28370  supadd  28371  ptrest  28378  heicant  28379  mblfinlem1  28381  mblfinlem3  28383  mblfinlem4  28384  ismblfin  28385  itg2addnclem  28396  itg2addnclem3  28398  itg2addnc  28399  itg2gt0cn  28400  cnicciblnc  28416  ftc1anclem6  28425  gtinf  28467  nn0prpwlem  28470  refssex  28506  fnessref  28518  islocfin  28521  locfinnei  28527  comppfsc  28532  neibastop2lem  28534  neibastop2  28535  tailfb  28551  unirep  28559  indexa  28580  sdclem2  28591  sdclem1  28592  sdc  28593  fdc  28594  fdc1  28595  incsequz  28597  istotbnd  28621  sstotbnd2  28626  equivtotbnd  28630  isbnd  28632  bndss  28638  ssbnd  28640  totbndbnd  28641  ismtybndlem  28658  heibor1lem  28661  heiborlem1  28663  heiborlem6  28668  heiborlem8  28670  heiborlem10  28672  heibor  28673  isdrngo2  28717  divrngidl  28781  prnc  28820  isfldidl  28821  prtlem5  28954  prtlem13  28966  prtlem16  28967  elrfi  28983  isnacs  28993  nacsfg  28994  nacsfix  29001  mzpcompact2lem  29041  eldiophb  29048  eldioph  29049  eldioph2  29053  eldioph2b  29054  eldioph3  29057  eldiophss  29066  diophrex  29067  sbc2rexgOLD  29079  rexrabdioph  29085  rexfrabdioph  29086  elnn0rabdioph  29094  dvdsrabdioph  29101  eldioph4b  29103  eldioph4i  29104  diophren  29105  rencldnfilem  29112  pell1234qrdich  29155  jm2.27  29310  expdiophlem1  29323  wepwsolem  29347  aomclem8  29367  islnr3  29424  lnr2i  29425  lpirlnr  29426  hbtlem1  29432  hbtlem2  29433  hbtlem7  29434  hbtlem4  29435  hbtlem5  29437  hbtlem6  29438  dgraaval  29454  dgraalem  29455  dgraaub  29458  rngunsnply  29483  infrglb  29724  climinf  29732  climinff  29737  stoweidlem27  29775  stoweidlem31  29779  stoweidlem43  29791  stoweidlem46  29794  stoweidlem52  29800  stoweidlem60  29808  cbvrex2  29950  afvelrnb  30022  afvelrnb0  30023  el2xptp  30079  rabasiun  30183  wwlkn0  30276  el2wlksot  30352  el2pthsot  30353  2wot2wont  30358  2spot2iun2spont  30363  cshwlemma1  30442  scshwfzeqfzo  30445  Lemma2  30446  erclwwlkneq  30450  eclclwwlkn0  30458  eleclclwwlkn  30460  hashecclwwlkn1  30461  usghashecclwwlk  30462  3cyclfrgrarn1  30557  usgn0fidegnn0  30575  frgrancvvdeqlem4  30579  friendshipgt3  30667  mat1dimelbas  30790  mat1dimbas  30791  scmatid  30805  scmatsubcl  30807  scmatmulcl  30809  pmatcollpw2lem  30820  lcoval  30835  el0ldep  30889  ldepspr  30896  grp1  30911  zlmodzxzldep  30935  bnj66  31740  bnj873  31804  bnj18eq1  31807  bnj1234  31891  bnj1318  31903  bj-finsumval0  32426  islshp  32464  lsmsat  32493  lcvbr  32506  lsatcv0  32516  lshpsmreu  32594  lshpkrlem1  32595  lshpkrlem2  32596  lshpkrlem3  32597  lshpkrcl  32601  lshpset2N  32604  islshpkrN  32605  cvrval  32754  atlex  32801  glbconxN  32862  hlsuprexch  32865  islln  32990  islpln  33014  islpln5  33019  lvolex3N  33022  islvol  33057  islvol5  33063  ispointN  33226  pmapglbx  33253  paddval  33282  elpaddn0  33284  elpaddat  33288  elpadd0  33293  4atex  33560  4atex2  33561  cdlemefrs29bpre1  33881  cdlemefrs32fva  33884  cdlemg33b  34191  dvhb1dimN  34470  dvhopellsm  34602  dib1dim  34650  diclspsn  34679  dihglblem2aN  34778  dihglblem2N  34779  dih1dimatlem  34814  dvh3dimatN  34924  dvh2dim  34930  dvh3dim  34931  dvh4dimN  34932  dvh3dim3N  34934  dochfl1  34961  lcfl7N  34986  lcf1o  35036  lcfrlem39  35066  mapdpglem3  35160  hvmapvalvalN  35246  hdmap14lem2a  35355  hdmapglem7a  35415