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

Theorem rexbidv 2663
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 1626 . 2  |-  F/ x ph
2 ralbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2rexbid 2661 1  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   E.wrex 2643
This theorem is referenced by:  rexbii  2667  2rexbidv  2685  rexralbidv  2686  rexeqbi1dv  2849  rexeqbidv  2853  cbvrex2v  2877  rspc2ev  2996  rspc3ev  2998  ceqsrex2v  3007  sbcrexg  3172  uniiunlem  3367  eliun  4032  dfiin2g  4059  orduninsuc  4756  elrnmpt  5050  elrnmptg  5053  elimag  5140  funcnvuni  5451  fun11iun  5628  fvelrnb  5706  fvelimab  5714  foelrn  5820  foco2  5821  elabrex  5917  abrexco  5918  abrexex2g  5920  abrexex2  5933  f1oiso  6003  f1oiso2  6004  f1oweALT  6006  grprinvlem  6217  recseq  6563  tfrlem3  6567  tfrlem3a  6568  tfrlem12  6579  seqomlem2  6637  nneob  6824  qseq2  6884  elqsg  6885  elixpsn  7030  ixpsnf1o  7031  isfi  7060  enfi  7254  pssnn  7256  frfi  7281  unblem1  7288  unblem2  7289  unbnn2  7293  fofinf1o  7316  finsschain  7341  indexfi  7342  elfi  7346  marypha1lem  7366  supmo  7383  suplub  7391  supisolem  7401  oieq1  7407  ordtypelem2  7414  ordtypelem3  7415  ordtypelem9  7421  wemaplem1  7441  brwdom2  7467  brwdom3  7476  unwdomg  7478  oemapval  7565  cantnf  7575  wemapwe  7580  cnfcom3clem  7588  tz9.13  7643  tz9.13g  7644  cardf2  7756  isnum2  7758  ennum  7760  cardiun  7795  infxpenc2  7829  aceq1  7924  aceq2  7926  dfac5lem3  7932  dfac5lem4  7933  dfac2a  7936  dfac2  7937  kmlem9  7964  kmlem12  7967  kmlem14  7969  ackbij1  8044  cflm  8056  cfss  8071  cofsmo  8075  cfsmolem  8076  cfcoflem  8078  coftr  8079  isfin7  8107  fin23lem26  8131  isf32lem5  8163  fin1a2lem11  8216  hsmexlem2  8233  axdc3lem3  8258  axdc3  8260  numthcor  8300  zorn2lem7  8308  brdom3  8332  brdom7disj  8335  brdom6disj  8336  iundom2g  8341  fpwwe2  8444  winainflem  8494  winalim2  8497  inar1  8576  tskuni  8584  nqereu  8732  prnmax  8798  genpv  8802  genpnmax  8810  genpass  8812  prlem936  8850  recexsrlem  8904  map2psrpr  8911  supsrlem  8912  axrrecex  8964  axpre-sup  8970  cnegex  9172  recex  9579  fimaxre3  9882  infm3  9892  supmul1  9898  supmullem1  9899  supmullem2  9900  supmul  9901  creur  9919  creui  9920  cju  9921  nnunb  10142  arch  10143  xrsupsslem  10810  xrinfmsslem  10811  xrsupss  10812  xrinfmss  10813  xrub  10815  supxrunb1  10823  supxrunb2  10824  infmxrgelb  10838  fsequb2  11235  iswrd  11649  wrdval  11650  shftfval  11805  abs1m  12059  rexfiuz  12071  limsupbnd2  12197  clim  12208  rlim  12209  rlim2  12210  rlim0  12222  rlim0lt  12223  ello1mpt2  12236  o1lo1  12251  o1compt  12301  rlimdiv  12359  climsup  12383  sumeq1f  12402  sumeq2w  12406  cbvsum  12409  summo  12431  fsum  12434  fsumcvg3  12443  infcvgaux2i  12557  mertenslem1  12581  mertenslem2  12582  mertens  12583  divides  12774  odd2np1lem  12827  divalglem4  12836  divalglem10  12842  divalg  12843  gcdcllem3  12933  bezoutlem1  12958  exprmfct  13030  opeo  13107  omeo  13108  pythagtriplem2  13111  pythagtrip  13128  pceu  13140  pcprmpw2  13175  unbenlem  13196  4sqlem12  13244  vdwapval  13261  vdwapun  13262  vdwmc2  13267  vdwpc  13268  vdwlem2  13270  vdwlem10  13278  vdwlem13  13281  vdwnnlem1  13283  rami  13303  brssc  13934  isdrs  14311  drsdir  14312  drsdirfi  14315  isdrs2  14316  ipodrsima  14511  spwpr4  14583  gsumvalx  14694  gsumpropd  14696  gsumress  14697  grpinvex  14740  imasgrp2  14853  conjnmzb  14960  gaorb  15004  orbsta  15010  ispgp  15146  subgpgp  15151  sylow1  15157  pgpfi  15159  sylow2blem3  15176  fislw  15179  sylow3lem2  15182  lsmelvalm  15205  lsmass  15222  pj1fval  15246  pj1val  15247  pj1eu  15248  pj1id  15251  efgrelexlema  15301  efgrelexlemb  15302  efgredeu  15304  cyggeninv  15413  cygabl  15420  pgpfac1lem2  15553  pgpfac1lem3  15555  pgpfac1lem4  15556  pgpfac1  15558  pgpfaclem2  15560  pgpfac  15562  dvdsrval  15670  dvdsr  15671  subrgdvds  15802  lss1d  15959  lspsn  15998  lspsnel  15999  lspsolvlem  16134  rspsn  16245  opsrval  16455  znf1o  16748  cygznlem3  16766  basis2  16932  eltg2  16939  tg2  16946  isclo  17067  neival  17082  isnei  17083  isneip  17085  restbas  17137  neitr  17159  cnpval  17215  iscnp  17216  cnpimaex  17235  lmbr  17237  lmbr2  17238  cnprest2  17269  lmff  17280  regsep  17313  pnrmopn  17322  nrmsep3  17334  isnrm2  17337  iscmp  17366  cmpsublem  17377  cmpsub  17378  tgcmp  17379  sscmp  17383  hauscmplem  17384  1stcclb  17421  1stcfb  17422  is2ndc  17423  2ndc1stc  17428  1stcrest  17430  2ndcctbss  17432  1stcelcls  17438  llyeq  17447  nllyeq  17448  hausllycmp  17471  lly1stc  17473  txbas  17513  ptval  17516  ptpjopn  17558  ptclsg  17561  txcnp  17566  ptcnp  17568  txrest  17577  ptrescn  17585  txcmp  17589  tx1stc  17596  xkococn  17606  kqreglem1  17687  fbasssin  17782  fbssfi  17783  fbssint  17784  fbun  17786  fgss2  17820  fgcl  17824  ufli  17860  fmfnfmlem3  17902  fbflim2  17923  hauspwpwf1  17933  flfneii  17938  flftg  17942  txflf  17952  fclscf  17971  alexsubb  17991  alexsubALT  17996  tsmssubm  18086  ustincl  18151  ustdiag  18152  ustinvel  18153  ustexhalf  18154  ust0  18163  trust  18173  elutop  18177  ucnval  18221  ucncn  18229  cfiluexsm  18234  cfiluweak  18239  blss  18339  imasf1oxms  18402  mopni  18405  metss  18421  metrest  18437  metcnp3  18453  cfilucfil  18472  metuel2  18478  nlmvscn  18587  nrginvrcn  18591  icccmplem1  18717  icccmplem2  18718  icccmp  18720  divcn  18762  cncfval  18782  elcncf2  18784  cncfmet  18802  cnheibor  18844  evth  18848  lebnumlem3  18852  lebnum  18853  xlebnum  18854  lebnumii  18855  ipcn  19064  lmmbr  19075  lmmbr2  19076  cfilfval  19081  cfili  19085  iscfil3  19090  caufval  19092  iscau  19093  iscau2  19094  equivcfil  19116  equivcau  19117  lmcau  19129  ovolval  19230  elovolm  19231  ovolgelb  19236  ovoliunlem1  19258  ovoliun2  19262  ovolshftlem1  19265  ovolscalem1  19269  ovolicc  19279  ioombl1lem4  19315  uniioombllem2  19335  mbfaddlem  19412  mbfsup  19416  mbfinf  19417  mbflimsup  19418  i1fmulc  19455  itg1climres  19466  itg2val  19480  itg2l  19481  itg2leub  19486  itg2seq  19494  itg2monolem1  19502  itg2mono  19505  itg2i1fseq2  19508  cniccibl  19592  ellimc3  19626  limciun  19641  dvferm1  19729  dvferm2  19731  lhop1lem  19757  ply1divex  19919  ig1peu  19954  plyval  19972  elply2  19975  coeval  20002  coeeu  20004  coelem  20005  coeeq  20006  plydivlem4  20073  plydivex  20074  aannenlem2  20106  aalioulem2  20110  aaliou2  20117  ulmval  20156  ulm2  20161  ulmcau  20171  ulmdvlem3  20178  abelthlem9  20216  abelth  20217  efif1olem4  20307  eflogeq  20356  efopn  20409  cxpcn3  20492  cxpeq  20501  rlimcnp  20664  muval  20775  dchrptlem1  20908  dchrptlem2  20909  lgsdchrval  20991  pntpbnd  21142  pntibndlem3  21146  pntibnd  21147  pntlemi  21158  pntleme  21162  pntlemp  21164  pnt3  21166  nbgraf1olem1  21310  cusgrafilem2  21348  cusgrafi  21350  iseupa  21528  isgrpo  21625  isgrpoi  21627  grpoidinvlem3  21635  grpoideu  21638  grpoidinv2  21647  isgrp2d  21664  isgrpda  21726  ghgrp  21797  rngoid  21812  nmoofval  22104  nmooval  22105  nmosetn0  22107  nmoolb  22113  nmoubi  22114  nmlno0lem  22135  chcompl  22586  pjhthmo  22645  pjhval  22740  pjpreeq  22741  h1de2ci  22899  elspansn  22909  nmopval  23200  nmopsetn0  23209  nmfnval  23220  nmfnsetn0  23222  eigvecval  23240  hhcno  23248  hhcnf  23249  nmoplb  23251  nmopub  23252  nmfnlb  23268  nmfnleub  23269  eleigvec  23301  nmlnop0iALT  23339  nmopun  23358  nmcexi  23370  branmfn  23449  pjnmopi  23492  cvbr  23626  hatomic  23704  chrelat2  23714  cdjreui  23776  cdj3lem2  23779  reuxfr4d  23814  elabreximd  23828  unipreima  23891  abfmpunirn  23899  curry2ima  23931  tpr2rico  24107  rge0scvg  24132  esumc  24235  esumpcvgval  24257  dya2icoseg2  24415  dya2iocuni  24420  lgamgulmlem6  24590  subfacp1lem3  24640  pconcn  24683  cnpcon  24689  txpcon  24691  conpcon  24694  iscvm  24718  cvmcov  24722  cvmopnlem  24737  cvmliftlem15  24757  cvmlift3lem2  24779  cvmlift3lem4  24781  cvmlift3  24787  dedekind  24959  prodeq1f  25006  prodeq2w  25010  prodmo  25034  fprod  25039  br8  25130  br6  25131  br4  25132  dfrdg2  25169  dfrdg3  25170  orderseqlem  25269  poseq  25270  soseq  25271  elno  25317  sltval  25318  nobndlem6  25368  nofulllem1  25373  nofulllem2  25374  nofulllem5  25377  altxpeq2  25526  brbtwn  25545  brcgr  25546  axpasch  25587  axlowdim2  25606  axlowdim  25607  axcontlem2  25611  axcontlem4  25613  axcontlem7  25616  axcontlem8  25617  funtransport  25672  fvtransport  25673  brcolinear2  25699  colineardim1  25702  segcon2  25746  brsegle  25749  funray  25781  fvray  25782  funline  25783  linedegen  25784  fvline  25785  ellines  25793  supaddc  25940  supadd  25941  itg2addnclem  25950  itg2addnc  25952  itg2gt0cn  25953  cnicciblnc  25969  gtinf  26006  nn0prpwlem  26009  refssex  26045  fnessref  26057  islocfin  26060  locfinnei  26066  comppfsc  26071  neibastop2lem  26073  neibastop2  26074  tailfb  26090  unirep  26098  indexa  26119  sdclem2  26130  sdclem1  26131  sdc  26132  fdc  26133  fdc1  26134  incsequz  26136  istotbnd  26162  sstotbnd2  26167  equivtotbnd  26171  isbnd  26173  bndss  26179  ssbnd  26181  totbndbnd  26182  ismtybndlem  26199  heibor1lem  26202  heiborlem1  26204  heiborlem6  26209  heiborlem8  26211  heiborlem10  26213  heibor  26214  isdrngo2  26258  divrngidl  26322  prnc  26361  isfldidl  26362  prtlem5  26389  prtlem13  26401  prtlem16  26402  elrfi  26432  isnacs  26442  nacsfg  26443  nacsfix  26450  mzpcompact2lem  26492  eldiophb  26499  eldioph  26500  eldioph2  26504  eldioph2b  26505  eldioph3  26508  eldiophss  26517  diophrex  26518  sbc2rexg  26528  rexrabdioph  26538  rexfrabdioph  26539  elnn0rabdioph  26547  dvdsrabdioph  26554  eldioph4b  26556  eldioph4i  26557  diophren  26558  rencldnfilem  26565  pell1234qrdich  26608  jm2.27  26763  expdiophlem1  26776  wepwsolem  26800  aomclem8  26821  ellspd  26916  islnr3  26981  lnr2i  26982  lpirlnr  26983  hbtlem1  26989  hbtlem2  26990  hbtlem7  26991  hbtlem4  26992  hbtlem5  26994  hbtlem6  26995  dgraaval  27011  dgraalem  27012  dgraaub  27015  rngunsnply  27040  psgnunilem3  27081  psgneu  27091  psgnval  27092  psgnvali  27093  psgnvalii  27094  infrglb  27383  climinf  27393  climinff  27398  stoweidlem27  27437  stoweidlem31  27441  stoweidlem43  27453  stoweidlem46  27456  stoweidlem52  27462  stoweidlem60  27470  cbvrex2  27612  afvelrnb  27689  afvelrnb0  27690  frgra2v  27745  3cyclfrgrarn1  27758  frgrancvvdeqlem4  27778  bnj66  28562  bnj873  28626  bnj18eq1  28629  bnj1234  28713  bnj1318  28725  islshp  29145  lsmsat  29174  lcvbr  29187  lsatcv0  29197  lshpsmreu  29275  lshpkrlem1  29276  lshpkrlem2  29277  lshpkrlem3  29278  lshpkrcl  29282  lshpset2N  29285  islshpkrN  29286  cvrval  29435  atlex  29482  glbconxN  29543  hlsuprexch  29546  islln  29671  islpln  29695  islpln5  29700  lvolex3N  29703  islvol  29738  islvol5  29744  ispointN  29907  pmapglbx  29934  paddval  29963  elpaddn0  29965  elpaddat  29969  elpadd0  29974  4atex  30241  4atex2  30242  cdlemefrs29bpre1  30562  cdlemefrs32fva  30565  cdlemg33b  30872  dvhb1dimN  31151  dvhopellsm  31283  dib1dim  31331  diclspsn  31360  dihglblem2aN  31459  dihglblem2N  31460  dih1dimatlem  31495  dvh3dimatN  31605  dvh2dim  31611  dvh3dim  31612  dvh4dimN  31613  dvh3dim3N  31615  dochfl1  31642  lcfl7N  31667  lcf1o  31717  lcfrlem39  31747  mapdpglem3  31841  hvmapvalvalN  31927  hdmap14lem2a  32036  hdmapglem7a  32096
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-rex 2648
  Copyright terms: Public domain W3C validator