MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexbidv Structured version   Unicode version

Theorem rexbidv 2726
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
StepHypRef Expression
1 nfv 1672 . 2  |-  F/ x ph
2 ralbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2rexbid 2724 1  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   E.wrex 2706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-rex 2711
This theorem is referenced by:  rexbii  2730  2rexbidv  2748  rexralbidv  2749  rexeqbi1dv  2916  rexeqbidv  2922  cbvrex2v  2946  rspc2ev  3070  rspc3ev  3072  ceqsrex2v  3084  sbcrexgOLD  3260  uniiunlem  3428  eliun  4163  dfiin2g  4191  dfiunv2  4194  elrnmpt  5073  elrnmptg  5076  elimag  5161  fvelrnb  5727  fvelimab  5735  foelrn  5850  foco2  5851  elabrex  5947  abrexco  5948  f1oiso  6029  f1oiso2  6030  grprinvlem  6290  orduninsuc  6443  funcnvuni  6519  fun11iun  6526  abrexex2g  6543  abrexex2  6547  f1oweALT  6550  recseq  6819  tfrlem12  6834  seqomlem2  6892  nneob  7079  qseq2  7139  elqsg  7140  elixpsn  7290  ixpsnf1o  7291  isfi  7321  enfi  7517  pssnn  7519  frfi  7545  unblem1  7552  unblem2  7553  unbnn2  7557  fofinf1o  7580  finsschain  7606  indexfi  7607  elfi  7651  marypha1lem  7671  supeq3  7687  supmo  7690  suplub  7698  supisolem  7708  oieq1  7714  ordtypelem2  7721  ordtypelem3  7722  ordtypelem9  7728  wemaplem1  7748  brwdom2  7776  brwdom3  7785  unwdomg  7787  oemapval  7879  cantnf  7889  cantnfOLD  7911  wemapwe  7916  wemapweOLD  7917  cnfcom3clem  7926  cnfcom3clemOLD  7934  tz9.13  7986  tz9.13g  7987  cardf2  8101  isnum2  8103  ennum  8105  cardiun  8140  infxpenc2  8176  infxpenc2OLD  8180  aceq1  8275  aceq2  8277  dfac5lem3  8283  dfac5lem4  8284  dfac2a  8287  dfac2  8288  kmlem9  8315  kmlem12  8318  kmlem14  8320  ackbij1  8395  cflm  8407  cfss  8422  cofsmo  8426  cfsmolem  8427  cfcoflem  8429  coftr  8430  isfin7  8458  fin23lem26  8482  isf32lem5  8514  fin1a2lem11  8567  hsmexlem2  8584  axdc3lem3  8609  axdc3  8611  numthcor  8651  zorn2lem7  8659  brdom3  8683  brdom7disj  8686  brdom6disj  8687  iundom2g  8692  fpwwe2  8798  winainflem  8848  winalim2  8851  inar1  8930  tskuni  8938  nqereu  9086  prnmax  9152  genpv  9156  genpnmax  9164  genpass  9166  prlem936  9204  recexsrlem  9258  map2psrpr  9265  supsrlem  9266  axrrecex  9318  axpre-sup  9324  dedekind  9521  cnegex  9538  recex  9956  fimaxre3  10267  infm3  10277  supmul1  10283  supmullem1  10284  supmullem2  10285  supmul  10286  creur  10304  creui  10305  cju  10306  nnunb  10563  arch  10564  xrsupsslem  11257  xrinfmsslem  11258  xrsupss  11259  xrinfmss  11260  xrub  11262  supxrunb1  11270  supxrunb2  11271  infmxrgelb  11285  fsequb2  11782  iswrd  12221  wrdval  12222  csbwrdg  12241  cshword  12412  0csh0  12414  shftfval  12543  abs1m  12807  rexfiuz  12819  limsupbnd2  12945  clim  12956  rlim  12957  rlim2  12958  rlim0  12970  rlim0lt  12971  ello1mpt2  12984  o1lo1  12999  o1compt  13049  rlimdiv  13107  climsup  13131  sumeq1  13150  sumeq2w  13153  summo  13178  fsum  13181  fsumcvg3  13190  infcvgaux2i  13303  mertenslem1  13327  mertenslem2  13328  mertens  13329  divides  13520  odd2np1lem  13574  divalglem4  13583  divalglem10  13589  divalg  13590  gcdcllem3  13680  bezoutlem1  13705  exprmfct  13779  nnnn0modprm0  13857  opeo  13863  omeo  13864  pythagtriplem2  13867  pythagtrip  13884  pceu  13896  pcprmpw2  13931  unbenlem  13952  4sqlem12  14000  vdwapval  14017  vdwapun  14018  vdwmc2  14023  vdwpc  14024  vdwlem2  14026  vdwlem10  14034  vdwlem13  14037  vdwnnlem1  14039  rami  14059  cshwsiun  14109  cshwrepswhash1  14112  brssc  14710  isdrs  15087  drsdir  15088  drsdirfi  15091  isdrs2  15092  ipodrsima  15318  gsumvalx  15484  gsumpropd  15486  gsumress  15487  grpinvex  15533  imasgrp2  15650  conjnmzb  15761  gaorb  15805  orbsta  15811  symgfix2  15901  symgextfo  15907  pmtrprfvalrn  15974  psgnunilem3  15982  psgneu  15992  psgnval  15993  psgnvali  15994  psgnvalii  15995  ispgp  16071  subgpgp  16076  sylow1  16082  pgpfi  16084  sylow2blem3  16101  fislw  16104  sylow3lem2  16107  lsmelvalm  16130  lsmass  16147  pj1fval  16171  pj1val  16172  pj1eu  16173  pj1id  16176  efgrelexlema  16226  efgrelexlemb  16227  efgredeu  16229  cyggeninv  16340  cygabl  16347  pgpfac1lem2  16550  pgpfac1lem3  16552  pgpfac1lem4  16553  pgpfac1  16555  pgpfaclem2  16557  pgpfac  16559  dvdsrval  16671  dvdsr  16672  subrgdvds  16803  lss1d  16966  lspsn  17005  lspsnel  17006  lspsolvlem  17145  rspsn  17258  opsrval  17488  znf1o  17826  cygznlem3  17844  psgndiflemA  17873  ellspd  18072  ellspdOLD  18073  basis2  18398  eltg2  18405  tg2  18412  isclo  18533  neival  18548  isnei  18549  isneip  18551  restbas  18604  neitr  18626  cnpval  18682  iscnp  18683  cnpimaex  18702  lmbr  18704  lmbr2  18705  cnprest2  18736  lmff  18747  regsep  18780  pnrmopn  18789  nrmsep3  18801  isnrm2  18804  iscmp  18833  cmpsublem  18844  cmpsub  18845  tgcmp  18846  sscmp  18850  hauscmplem  18851  1stcclb  18890  1stcfb  18891  is2ndc  18892  2ndc1stc  18897  1stcrest  18899  2ndcctbss  18901  1stcelcls  18907  llyeq  18916  nllyeq  18917  hausllycmp  18940  lly1stc  18942  txbas  18982  ptval  18985  ptpjopn  19027  ptclsg  19030  txcnp  19035  ptcnp  19037  txrest  19046  ptrescn  19054  txcmp  19058  tx1stc  19065  xkococn  19075  kqreglem1  19156  fbasssin  19251  fbssfi  19252  fbssint  19253  fbun  19255  fgss2  19289  fgcl  19293  ufli  19329  fmfnfmlem3  19371  fbflim2  19392  hauspwpwf1  19402  flfneii  19407  flftg  19411  txflf  19421  fclscf  19440  alexsubb  19460  alexsubALT  19465  tsmssubm  19558  ustincl  19624  ustdiag  19625  ustinvel  19626  ustexhalf  19627  ust0  19636  trust  19646  elutop  19650  ucnval  19694  ucncn  19702  cfiluexsm  19707  cfiluweak  19712  blssps  19841  blss  19842  imasf1oxms  19906  mopni  19909  metss  19925  metrest  19941  metcnp3  19957  cfilucfilOLD  19986  cfilucfil  19987  metuel2  19996  nlmvscn  20110  nrginvrcn  20114  icccmplem1  20241  icccmplem2  20242  icccmp  20244  divcn  20286  cncfval  20306  elcncf2  20308  cncfmet  20326  cnheibor  20369  evth  20373  lebnumlem3  20377  lebnum  20378  xlebnum  20379  lebnumii  20380  ipcn  20600  lmmbr  20611  lmmbr2  20612  cfilfval  20617  cfili  20621  iscfil3  20626  caufval  20628  iscau  20629  iscau2  20630  equivcfil  20652  equivcau  20653  lmcau  20665  ovolval  20799  elovolm  20800  ovolgelb  20805  ovoliunlem1  20827  ovoliun2  20831  ovolshftlem1  20834  ovolscalem1  20838  ovolicc  20848  ioombl1lem4  20884  uniioombllem2  20905  mbfaddlem  20980  mbfsup  20984  mbfinf  20985  mbflimsup  20986  i1fmulc  21023  itg1climres  21034  itg2val  21048  itg2l  21049  itg2leub  21054  itg2seq  21062  itg2monolem1  21070  itg2mono  21073  itg2i1fseq2  21076  cniccibl  21160  ellimc3  21196  limciun  21211  dvferm1  21299  dvferm2  21301  lhop1lem  21327  ply1divex  21493  ig1peu  21528  plyval  21546  elply2  21549  coeval  21576  coeeu  21578  coelem  21579  coeeq  21580  plydivlem4  21647  plydivex  21648  aannenlem2  21680  aalioulem2  21684  aaliou2  21691  ulmval  21730  ulm2  21735  ulmcau  21745  ulmdvlem3  21752  abelthlem9  21790  abelth  21791  efif1olem4  21886  eflogeq  21935  efopn  21988  cxpcn3  22071  cxpeq  22080  rlimcnp  22244  muval  22355  dchrptlem1  22488  dchrptlem2  22489  lgsdchrval  22571  pntpbnd  22722  pntibndlem3  22726  pntibnd  22727  pntlemi  22738  pntleme  22742  pntlemp  22744  pnt3  22746  axtgsegcon  22810  axtgpasch  22813  axtgcont1  22814  legov  22892  ttgval  22944  ttgitvval  22951  ttgelitv  22952  brbtwn  22968  brcgr  22969  axpasch  23010  axlowdim2  23029  axlowdim  23030  axcontlem2  23034  axcontlem4  23036  axcontlem7  23039  axcontlem8  23040  nbgraf1olem1  23173  cusgrafilem2  23211  cusgrafi  23213  iseupa  23409  isgrpo  23506  isgrpoi  23508  grpoidinvlem3  23516  grpoideu  23519  grpoidinv2  23528  isgrp2d  23545  isgrpda  23607  ghgrp  23678  rngoid  23693  nmoofval  23985  nmooval  23986  nmosetn0  23988  nmoolb  23994  nmoubi  23995  nmlno0lem  24016  chcompl  24468  pjhthmo  24528  pjhval  24623  pjpreeq  24624  h1de2ci  24782  elspansn  24792  nmopval  25083  nmopsetn0  25092  nmfnval  25103  nmfnsetn0  25105  eigvecval  25123  hhcno  25131  hhcnf  25132  nmoplb  25134  nmopub  25135  nmfnlb  25151  nmfnleub  25152  eleigvec  25184  nmlnop0iALT  25222  nmopun  25241  nmcexi  25253  branmfn  25332  pjnmopi  25375  cvbr  25509  hatomic  25587  chrelat2  25597  cdjreui  25659  cdj3lem2  25662  reuxfr4d  25698  elabreximd  25715  br8d  25766  unipreima  25785  abfmpunirn  25791  curry2ima  25827  toslublem  25951  tosglblem  25953  archirng  26029  archiexdiv  26031  archiabllem2a  26035  archiabl  26039  isarchiofld  26138  pstmfval  26177  tpr2rico  26196  rge0scvg  26233  esumc  26359  esumpcvgval  26381  dya2icoseg2  26547  dya2iocuni  26552  eulerpartlemgvv  26607  eulerpartlemgh  26609  lgamgulmlem6  26868  subfacp1lem3  26918  pconcn  26961  cnpcon  26967  txpcon  26969  conpcon  26972  iscvm  26996  cvmcov  27000  cvmopnlem  27015  cvmliftlem15  27035  cvmlift3lem2  27057  cvmlift3lem4  27059  cvmlift3  27065  prodeq1f  27268  prodeq2w  27272  prodmo  27296  fprod  27301  br8  27413  br6  27414  br4  27415  dfrdg2  27456  dfrdg3  27457  orderseqlem  27560  poseq  27561  soseq  27562  elno  27634  sltval  27635  nobndlem6  27685  nofulllem1  27690  nofulllem2  27691  nofulllem5  27694  altxpeq2  27852  funtransport  27909  fvtransport  27910  brcolinear2  27936  colineardim1  27939  segcon2  27983  brsegle  27986  funray  28018  fvray  28019  funline  28020  linedegen  28021  fvline  28022  ellines  28030  supaddc  28261  supadd  28262  ptrest  28269  heicant  28270  mblfinlem1  28272  mblfinlem3  28274  mblfinlem4  28275  ismblfin  28276  itg2addnclem  28287  itg2addnclem3  28289  itg2addnc  28290  itg2gt0cn  28291  cnicciblnc  28307  ftc1anclem6  28316  gtinf  28358  nn0prpwlem  28361  refssex  28397  fnessref  28409  islocfin  28412  locfinnei  28418  comppfsc  28423  neibastop2lem  28425  neibastop2  28426  tailfb  28442  unirep  28450  indexa  28471  sdclem2  28482  sdclem1  28483  sdc  28484  fdc  28485  fdc1  28486  incsequz  28488  istotbnd  28512  sstotbnd2  28517  equivtotbnd  28521  isbnd  28523  bndss  28529  ssbnd  28531  totbndbnd  28532  ismtybndlem  28549  heibor1lem  28552  heiborlem1  28554  heiborlem6  28559  heiborlem8  28561  heiborlem10  28563  heibor  28564  isdrngo2  28608  divrngidl  28672  prnc  28711  isfldidl  28712  prtlem5  28846  prtlem13  28858  prtlem16  28859  elrfi  28875  isnacs  28885  nacsfg  28886  nacsfix  28893  mzpcompact2lem  28933  eldiophb  28940  eldioph  28941  eldioph2  28945  eldioph2b  28946  eldioph3  28949  eldiophss  28958  diophrex  28959  sbc2rexgOLD  28971  rexrabdioph  28977  rexfrabdioph  28978  elnn0rabdioph  28986  dvdsrabdioph  28993  eldioph4b  28995  eldioph4i  28996  diophren  28997  rencldnfilem  29004  pell1234qrdich  29047  jm2.27  29202  expdiophlem1  29215  wepwsolem  29239  aomclem8  29259  islnr3  29316  lnr2i  29317  lpirlnr  29318  hbtlem1  29324  hbtlem2  29325  hbtlem7  29326  hbtlem4  29327  hbtlem5  29329  hbtlem6  29330  dgraaval  29346  dgraalem  29347  dgraaub  29350  rngunsnply  29375  infrglb  29617  climinf  29625  climinff  29630  stoweidlem27  29668  stoweidlem31  29672  stoweidlem43  29684  stoweidlem46  29687  stoweidlem52  29693  stoweidlem60  29701  cbvrex2  29843  afvelrnb  29915  afvelrnb0  29916  el2xptp  29972  rabasiun  30076  wwlkn0  30169  el2wlksot  30245  el2pthsot  30246  2wot2wont  30251  2spot2iun2spont  30256  cshwlemma1  30335  scshwfzeqfzo  30338  Lemma2  30339  erclwwlkneq  30343  eclclwwlkn0  30351  eleclclwwlkn  30353  hashecclwwlkn1  30354  usghashecclwwlk  30355  3cyclfrgrarn1  30450  usgn0fidegnn0  30468  frgrancvvdeqlem4  30472  friendshipgt3  30560  lcoval  30655  el0ldep  30709  ldepspr  30716  grp1  30731  zlmodzxzldep  30755  bnj66  31555  bnj873  31619  bnj18eq1  31622  bnj1234  31706  bnj1318  31718  bj-finsumval0  32159  islshp  32197  lsmsat  32226  lcvbr  32239  lsatcv0  32249  lshpsmreu  32327  lshpkrlem1  32328  lshpkrlem2  32329  lshpkrlem3  32330  lshpkrcl  32334  lshpset2N  32337  islshpkrN  32338  cvrval  32487  atlex  32534  glbconxN  32595  hlsuprexch  32598  islln  32723  islpln  32747  islpln5  32752  lvolex3N  32755  islvol  32790  islvol5  32796  ispointN  32959  pmapglbx  32986  paddval  33015  elpaddn0  33017  elpaddat  33021  elpadd0  33026  4atex  33293  4atex2  33294  cdlemefrs29bpre1  33614  cdlemefrs32fva  33617  cdlemg33b  33924  dvhb1dimN  34203  dvhopellsm  34335  dib1dim  34383  diclspsn  34412  dihglblem2aN  34511  dihglblem2N  34512  dih1dimatlem  34547  dvh3dimatN  34657  dvh2dim  34663  dvh3dim  34664  dvh4dimN  34665  dvh3dim3N  34667  dochfl1  34694  lcfl7N  34719  lcf1o  34769  lcfrlem39  34799  mapdpglem3  34893  hvmapvalvalN  34979  hdmap14lem2a  35088  hdmapglem7a  35148
  Copyright terms: Public domain W3C validator