Theorem rexbidv 2844

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

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		nfv 1674	. 2 |- F/ x ph
2		rexbidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	rexbid 2843	1 |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591  df-rex 2801

This theorem is referenced by:  rexbii  2847  2rexbidv  2862  rexralbidv  2863  rexeqbi1dv  3022  rexeqbidv  3028  cbvrex2v  3052  rspc2ev  3178  rspc3ev  3180  ceqsrex2v  3192  sbcrexgOLD  3370  uniiunlem  3538  eliun  4273  dfiin2g  4301  dfiunv2  4304  elrnmpt  5184  elrnmptg  5187  elimag  5271  fvelrnb  5838  fvelimab  5846  foelrn  5961  foco2  5962  elabrex  6059  abrexco  6060  f1oiso  6141  f1oiso2  6142  grprinvlem  6401  orduninsuc  6554  funcnvuni  6630  fun11iun  6637  abrexex2g  6654  abrexex2  6658  f1oweALT  6661  recseq  6933  tfrlem12  6948  seqomlem2  7006  nneob  7191  qseq2  7251  elqsg  7252  elixpsn  7402  ixpsnf1o  7403  isfi  7433  enfi  7630  pssnn  7632  frfi  7658  unblem1  7665  unblem2  7666  unbnn2  7670  fofinf1o  7693  finsschain  7719  indexfi  7720  elfi  7764  marypha1lem  7784  supeq3  7800  supmo  7803  suplub  7811  supisolem  7821  oieq1  7827  ordtypelem2  7834  ordtypelem3  7835  ordtypelem9  7841  wemaplem1  7861  brwdom2  7889  brwdom3  7898  unwdomg  7900  oemapval  7992  cantnf  8002  cantnfOLD  8024  wemapwe  8029  wemapweOLD  8030  cnfcom3clem  8039  cnfcom3clemOLD  8047  tz9.13  8099  tz9.13g  8100  cardf2  8214  isnum2  8216  ennum  8218  cardiun  8253  infxpenc2  8289  infxpenc2OLD  8293  aceq1  8388  aceq2  8390  dfac5lem3  8396  dfac5lem4  8397  dfac2a  8400  dfac2  8401  kmlem9  8428  kmlem12  8431  kmlem14  8433  ackbij1  8508  cflm  8520  cfss  8535  cofsmo  8539  cfsmolem  8540  cfcoflem  8542  coftr  8543  isfin7  8571  fin23lem26  8595  isf32lem5  8627  fin1a2lem11  8680  hsmexlem2  8697  axdc3lem3  8722  axdc3  8724  numthcor  8764  zorn2lem7  8772  brdom3  8796  brdom7disj  8799  brdom6disj  8800  iundom2g  8805  fpwwe2  8911  winainflem  8961  winalim2  8964  inar1  9043  tskuni  9051  nqereu  9199  prnmax  9265  genpv  9269  genpnmax  9277  genpass  9279  prlem936  9317  recexsrlem  9371  map2psrpr  9378  supsrlem  9379  axrrecex  9431  axpre-sup  9437  dedekind  9634  cnegex  9651  recex  10069  fimaxre3  10380  infm3  10390  supmul1  10396  supmullem1  10397  supmullem2  10398  supmul  10399  creur  10417  creui  10418  cju  10419  nnunb  10676  arch  10677  xrsupsslem  11370  xrinfmsslem  11371  xrsupss  11372  xrinfmss  11373  xrub  11375  supxrunb1  11383  supxrunb2  11384  infmxrgelb  11398  fsequb2  11899  iswrd  12339  wrdval  12340  csbwrdg  12359  cshword  12530  0csh0  12532  shftfval  12661  abs1m  12925  rexfiuz  12937  limsupbnd2  13063  clim  13074  rlim  13075  rlim2  13076  rlim0  13088  rlim0lt  13089  ello1mpt2  13102  o1lo1  13117  o1compt  13167  rlimdiv  13225  climsup  13249  sumeq1  13268  sumeq2w  13271  summo  13296  fsum  13299  fsumcvg3  13308  infcvgaux2i  13422  mertenslem1  13446  mertenslem2  13447  mertens  13448  divides  13639  odd2np1lem  13693  divalglem4  13702  divalglem10  13708  divalg  13709  gcdcllem3  13799  bezoutlem1  13824  exprmfct  13898  nnnn0modprm0  13976  opeo  13982  omeo  13983  pythagtriplem2  13986  pythagtrip  14003  pceu  14015  pcprmpw2  14050  unbenlem  14071  4sqlem12  14119  vdwapval  14136  vdwapun  14137  vdwmc2  14142  vdwpc  14143  vdwlem2  14145  vdwlem10  14153  vdwlem13  14156  vdwnnlem1  14158  rami  14178  cshwsiun  14228  cshwrepswhash1  14231  brssc  14829  isdrs  15206  drsdir  15207  drsdirfi  15210  isdrs2  15211  ipodrsima  15437  gsumvalx  15604  gsumpropd  15606  gsumress  15609  grpinvex  15655  imasgrp2  15772  conjnmzb  15883  gaorb  15927  orbsta  15933  symgfix2  16023  symgextfo  16029  pmtrprfvalrn  16096  psgnunilem3  16104  psgneu  16114  psgnval  16115  psgnvali  16116  psgnvalii  16117  ispgp  16195  subgpgp  16200  sylow1  16206  pgpfi  16208  sylow2blem3  16225  fislw  16228  sylow3lem2  16231  lsmelvalm  16254  lsmass  16271  pj1fval  16295  pj1val  16296  pj1eu  16297  pj1id  16300  efgrelexlema  16350  efgrelexlemb  16351  efgredeu  16353  cyggeninv  16464  cygabl  16471  pgpfac1lem2  16681  pgpfac1lem3  16683  pgpfac1lem4  16684  pgpfac1  16686  pgpfaclem2  16688  pgpfac  16690  dvdsrval  16843  dvdsr  16844  subrgdvds  16985  lss1d  17150  lspsn  17189  lspsnel  17190  lspsolvlem  17329  rspsn  17442  opsrval  17663  znf1o  18093  cygznlem3  18111  psgndiflemA  18140  ellspd  18339  ellspdOLD  18340  basis2  18672  eltg2  18679  tg2  18686  isclo  18807  neival  18822  isnei  18823  isneip  18825  restbas  18878  neitr  18900  cnpval  18956  iscnp  18957  cnpimaex  18976  lmbr  18978  lmbr2  18979  cnprest2  19010  lmff  19021  regsep  19054  pnrmopn  19063  nrmsep3  19075  isnrm2  19078  iscmp  19107  cmpsublem  19118  cmpsub  19119  tgcmp  19120  sscmp  19124  hauscmplem  19125  1stcclb  19164  1stcfb  19165  is2ndc  19166  2ndc1stc  19171  1stcrest  19173  2ndcctbss  19175  1stcelcls  19181  llyeq  19190  nllyeq  19191  hausllycmp  19214  lly1stc  19216  txbas  19256  ptval  19259  ptpjopn  19301  ptclsg  19304  txcnp  19309  ptcnp  19311  txrest  19320  ptrescn  19328  txcmp  19332  tx1stc  19339  xkococn  19349  kqreglem1  19430  fbasssin  19525  fbssfi  19526  fbssint  19527  fbun  19529  fgss2  19563  fgcl  19567  ufli  19603  fmfnfmlem3  19645  fbflim2  19666  hauspwpwf1  19676  flfneii  19681  flftg  19685  txflf  19695  fclscf  19714  alexsubb  19734  alexsubALT  19739  tsmssubm  19832  ustincl  19898  ustdiag  19899  ustinvel  19900  ustexhalf  19901  ust0  19910  trust  19920  elutop  19924  ucnval  19968  ucncn  19976  cfiluexsm  19981  cfiluweak  19986  blssps  20115  blss  20116  imasf1oxms  20180  mopni  20183  metss  20199  metrest  20215  metcnp3  20231  cfilucfilOLD  20260  cfilucfil  20261  metuel2  20270  nlmvscn  20384  nrginvrcn  20388  icccmplem1  20515  icccmplem2  20516  icccmp  20518  divcn  20560  cncfval  20580  elcncf2  20582  cncfmet  20600  cnheibor  20643  evth  20647  lebnumlem3  20651  lebnum  20652  xlebnum  20653  lebnumii  20654  ipcn  20874  lmmbr  20885  lmmbr2  20886  cfilfval  20891  cfili  20895  iscfil3  20900  caufval  20902  iscau  20903  iscau2  20904  equivcfil  20926  equivcau  20927  lmcau  20939  ovolval  21073  elovolm  21074  ovolgelb  21079  ovoliunlem1  21101  ovoliun2  21105  ovolshftlem1  21108  ovolscalem1  21112  ovolicc  21122  ioombl1lem4  21158  uniioombllem2  21179  mbfaddlem  21254  mbfsup  21258  mbfinf  21259  mbflimsup  21260  i1fmulc  21297  itg1climres  21308  itg2val  21322  itg2l  21323  itg2leub  21328  itg2seq  21336  itg2monolem1  21344  itg2mono  21347  itg2i1fseq2  21350  cniccibl  21434  ellimc3  21470  limciun  21485  dvferm1  21573  dvferm2  21575  lhop1lem  21601  ply1divex  21724  ig1peu  21759  plyval  21777  elply2  21780  coeval  21807  coeeu  21809  coelem  21810  coeeq  21811  plydivlem4  21878  plydivex  21879  aannenlem2  21911  aalioulem2  21915  aaliou2  21922  ulmval  21961  ulm2  21966  ulmcau  21976  ulmdvlem3  21983  abelthlem9  22021  abelth  22022  efif1olem4  22117  eflogeq  22166  efopn  22219  cxpcn3  22302  cxpeq  22311  rlimcnp  22475  muval  22586  dchrptlem1  22719  dchrptlem2  22720  lgsdchrval  22802  pntpbnd  22953  pntibndlem3  22957  pntibnd  22958  pntlemi  22969  pntleme  22973  pntlemp  22975  pnt3  22977  istrkgld  23037  axtgsegcon  23041  axtgpasch  23044  axtgcont1  23045  legov  23137  ttgval  23256  ttgitvval  23263  ttgelitv  23264  brbtwn  23280  brcgr  23281  axpasch  23322  axlowdim2  23341  axlowdim  23342  axcontlem2  23346  axcontlem4  23348  axcontlem7  23351  axcontlem8  23352  nbgraf1olem1  23485  cusgrafilem2  23523  cusgrafi  23525  iseupa  23721  isgrpo  23818  isgrpoi  23820  grpoidinvlem3  23828  grpoideu  23831  grpoidinv2  23840  isgrp2d  23857  isgrpda  23919  ghgrp  23990  rngoid  24005  nmoofval  24297  nmooval  24298  nmosetn0  24300  nmoolb  24306  nmoubi  24307  nmlno0lem  24328  chcompl  24780  pjhthmo  24840  pjhval  24935  pjpreeq  24936  h1de2ci  25094  elspansn  25104  nmopval  25395  nmopsetn0  25404  nmfnval  25415  nmfnsetn0  25417  eigvecval  25435  hhcno  25443  hhcnf  25444  nmoplb  25446  nmopub  25447  nmfnlb  25463  nmfnleub  25464  eleigvec  25496  nmlnop0iALT  25534  nmopun  25553  nmcexi  25565  branmfn  25644  pjnmopi  25687  cvbr  25821  hatomic  25899  chrelat2  25909  cdjreui  25971  cdj3lem2  25974  reuxfr4d  26009  elabreximd  26026  br8d  26076  unipreima  26095  abfmpunirn  26101  curry2ima  26137  toslublem  26262  tosglblem  26264  archirng  26339  archiexdiv  26341  archiabllem2a  26345  archiabl  26349  isarchiofld  26419  pstmfval  26457  tpr2rico  26476  rge0scvg  26513  esumc  26639  esumpcvgval  26661  dya2icoseg2  26827  dya2iocuni  26832  eulerpartlemgvv  26893  eulerpartlemgh  26895  lgamgulmlem6  27154  subfacp1lem3  27204  pconcn  27247  cnpcon  27253  txpcon  27255  conpcon  27258  iscvm  27282  cvmcov  27286  cvmopnlem  27301  cvmliftlem15  27321  cvmlift3lem2  27343  cvmlift3lem4  27345  cvmlift3  27351  prodeq1f  27555  prodeq2w  27559  prodmo  27583  fprod  27588  br8  27700  br6  27701  br4  27702  dfrdg2  27743  dfrdg3  27744  orderseqlem  27847  poseq  27848  soseq  27849  elno  27921  sltval  27922  nobndlem6  27972  nofulllem1  27977  nofulllem2  27978  nofulllem5  27981  altxpeq2  28139  funtransport  28196  fvtransport  28197  brcolinear2  28223  colineardim1  28226  segcon2  28270  brsegle  28273  funray  28305  fvray  28306  funline  28307  linedegen  28308  fvline  28309  ellines  28317  supaddc  28555  supadd  28556  ptrest  28563  heicant  28564  mblfinlem1  28566  mblfinlem3  28568  mblfinlem4  28569  ismblfin  28570  itg2addnclem  28581  itg2addnclem3  28583  itg2addnc  28584  itg2gt0cn  28585  cnicciblnc  28601  ftc1anclem6  28610  gtinf  28652  nn0prpwlem  28655  refssex  28691  fnessref  28703  islocfin  28706  locfinnei  28712  comppfsc  28717  neibastop2lem  28719  neibastop2  28720  tailfb  28736  unirep  28744  indexa  28765  sdclem2  28776  sdclem1  28777  sdc  28778  fdc  28779  fdc1  28780  incsequz  28782  istotbnd  28806  sstotbnd2  28811  equivtotbnd  28815  isbnd  28817  bndss  28823  ssbnd  28825  totbndbnd  28826  ismtybndlem  28843  heibor1lem  28846  heiborlem1  28848  heiborlem6  28853  heiborlem8  28855  heiborlem10  28857  heibor  28858  isdrngo2  28902  divrngidl  28966  prnc  29005  isfldidl  29006  prtlem5  29139  prtlem13  29151  prtlem16  29152  elrfi  29168  isnacs  29178  nacsfg  29179  nacsfix  29186  mzpcompact2lem  29226  eldiophb  29233  eldioph  29234  eldioph2  29238  eldioph2b  29239  eldioph3  29242  eldiophss  29251  diophrex  29252  sbc2rexgOLD  29264  rexrabdioph  29270  rexfrabdioph  29271  elnn0rabdioph  29279  dvdsrabdioph  29286  eldioph4b  29288  eldioph4i  29289  diophren  29290  rencldnfilem  29297  pell1234qrdich  29340  jm2.27  29495  expdiophlem1  29508  wepwsolem  29532  aomclem8  29552  islnr3  29609  lnr2i  29610  lpirlnr  29611  hbtlem1  29617  hbtlem2  29618  hbtlem7  29619  hbtlem4  29620  hbtlem5  29622  hbtlem6  29623  dgraaval  29639  dgraalem  29640  dgraaub  29643  rngunsnply  29668  infrglb  29909  climinf  29917  climinff  29922  stoweidlem27  29960  stoweidlem31  29964  stoweidlem43  29976  stoweidlem46  29979  stoweidlem52  29985  stoweidlem60  29993  cbvrex2  30135  afvelrnb  30207  afvelrnb0  30208  el2xptp  30264  rabasiun  30368  wwlkn0  30461  el2wlksot  30537  el2pthsot  30538  2wot2wont  30543  2spot2iun2spont  30548  cshwlemma1  30627  scshwfzeqfzo  30630  Lemma2  30631  erclwwlkneq  30635  eclclwwlkn0  30643  eleclclwwlkn  30645  hashecclwwlkn1  30646  usghashecclwwlk  30647  3cyclfrgrarn1  30742  usgn0fidegnn0  30760  frgrancvvdeqlem4  30764  friendshipgt3  30852  scmatscmid  31011  scmatscmids  31014  mat1dimelbas  31021  mat1dimbas  31022  scmatid  31036  scmatsubcl  31038  scmatmulcl  31040  lcoval  31053  el0ldep  31107  ldepspr  31114  grp1  31129  zlmodzxzldep  31153  pmatcollpwlem  31233  pmatcollpw1aa0  31235  pmattomply1mhmlem0  31272  pmattomply1mhmlem1  31273  cpscmat  31296  bnj66  32153  bnj873  32217  bnj18eq1  32220  bnj1234  32304  bnj1318  32316  bj-finsumval0  32889  islshp  32930  lsmsat  32959  lcvbr  32972  lsatcv0  32982  lshpsmreu  33060  lshpkrlem1  33061  lshpkrlem2  33062  lshpkrlem3  33063  lshpkrcl  33067  lshpset2N  33070  islshpkrN  33071  cvrval  33220  atlex  33267  glbconxN  33328  hlsuprexch  33331  islln  33456  islpln  33480  islpln5  33485  lvolex3N  33488  islvol  33523  islvol5  33529  ispointN  33692  pmapglbx  33719  paddval  33748  elpaddn0  33750  elpaddat  33754  elpadd0  33759  4atex  34026  4atex2  34027  cdlemefrs29bpre1  34347  cdlemefrs32fva  34350  cdlemg33b  34657  dvhb1dimN  34936  dvhopellsm  35068  dib1dim  35116  diclspsn  35145  dihglblem2aN  35244  dihglblem2N  35245  dih1dimatlem  35280  dvh3dimatN  35390  dvh2dim  35396  dvh3dim  35397  dvh4dimN  35398  dvh3dim3N  35400  dochfl1  35427  lcfl7N  35452  lcf1o  35502  lcfrlem39  35532  mapdpglem3  35626  hvmapvalvalN  35712  hdmap14lem2a  35821  hdmapglem7a  35881