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

Theorem rexbidv 3034
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 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
rexbidv (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rexbidv
StepHypRef Expression
1 rexbidv.1 . . 3 (𝜑 → (𝜓𝜒))
21adantr 480 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32rexbidva 3031 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wcel 1977  wrex 2897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-rex 2902
This theorem is referenced by:  2rexbidv  3039  rexralbidv  3040  rexeqbi1dv  3124  rexeqbidv  3130  cbvrex2v  3156  rspc2ev  3295  rspc3ev  3297  ceqsrex2v  3308  uniiunlem  3653  n0snor2el  4304  rabasiun  4459  eliun  4460  dfiin2g  4489  dfiunv2  4492  elrnmpt  5293  elrnmptg  5296  elimag  5389  fvelrnb  6153  fvelimab  6163  foelrn  6286  foco2  6287  foco2OLD  6288  elabrex  6405  abrexco  6406  f1oiso  6501  f1oiso2  6502  grprinvlem  6770  orduninsuc  6935  funcnvuni  7012  fun11iun  7019  abrexex2g  7036  abrexex2  7040  f1oweALT  7043  el2xptp  7102  tfrlem12  7372  seqomlem2  7433  nneob  7619  qseq2  7684  elqsg  7685  elqsecl  7688  elixpsn  7833  ixpsnf1o  7834  isfi  7865  enfi  8061  pssnn  8063  frfi  8090  unblem1  8097  unblem2  8098  unbnn2  8102  fofinf1o  8126  finsschain  8156  indexfi  8157  elfi  8202  marypha1lem  8222  supeq3  8238  supmo  8241  suplub  8249  supisolem  8262  eqinf  8273  infval  8275  infglb  8279  infglbb  8280  infmo  8284  oieq1  8300  ordtypelem2  8307  ordtypelem3  8308  ordtypelem9  8314  wemaplem1  8334  brwdom2  8361  brwdom3  8370  unwdomg  8372  oemapval  8463  cantnf  8473  wemapwe  8477  cnfcom3clem  8485  tz9.13  8537  tz9.13g  8538  cardf2  8652  isnum2  8654  ennum  8656  cardiun  8691  infxpenc2  8728  aceq1  8823  aceq2  8825  dfac5lem3  8831  dfac5lem4  8832  dfac2a  8835  dfac2  8836  kmlem9  8863  kmlem12  8866  kmlem14  8868  ackbij1  8943  cflm  8955  cfss  8970  cofsmo  8974  cfsmolem  8975  cfcoflem  8977  coftr  8978  isfin7  9006  fin23lem26  9030  isf32lem5  9062  fin1a2lem11  9115  hsmexlem2  9132  axdc3lem3  9157  axdc3  9159  numthcor  9199  zorn2lem7  9207  brdom3  9231  brdom7disj  9234  brdom6disj  9235  iundom2g  9241  fpwwe2  9344  winainflem  9394  winalim2  9397  inar1  9476  tskuni  9484  nqereu  9630  prnmax  9696  genpv  9700  genpnmax  9708  genpass  9710  prlem936  9748  recexsrlem  9803  map2psrpr  9810  supsrlem  9811  axrrecex  9863  axpre-sup  9869  dedekind  10079  cnegex  10096  recex  10538  fimaxre3  10849  infm3  10861  supaddc  10867  supadd  10868  supmul1  10869  supmullem1  10870  supmullem2  10871  supmul  10872  creur  10891  creui  10892  cju  10893  nnunb  11165  arch  11166  xrsupsslem  12009  xrinfmsslem  12010  xrsupss  12011  xrinfmss  12012  xrub  12014  supxrunb1  12021  supxrunb2  12022  infmremnf  12044  infmrp1  12045  modmuladd  12574  fsequb2  12637  hashge2el2difr  13118  iswrd  13162  wrdval  13163  csbwrdg  13189  cshword  13388  0csh0  13390  2cshwcshw  13422  scshwfzeqfzo  13423  cshimadifsn  13426  shftfval  13658  abs1m  13923  rexfiuz  13935  limsupbnd2  14062  clim  14073  rlim  14074  rlim2  14075  rlim0  14087  rlim0lt  14088  ello1mpt2  14101  o1lo1  14116  o1compt  14166  rlimdiv  14224  climsup  14248  sumeq1  14267  sumeq2w  14270  summo  14295  fsum  14298  fsumcvg3  14307  infcvgaux2i  14429  mertenslem1  14455  mertenslem2  14456  mertens  14457  prodeq1f  14477  prodeq2w  14481  prodmo  14505  fprod  14510  divides  14823  odd2np1lem  14902  opeo  14927  omeo  14928  divalglem4  14957  divalglem10  14963  divalg  14964  gcdcllem3  15061  zeqzmulgcd  15070  bezoutlem1  15094  exprmfct  15254  nnnn0modprm0  15349  pythagtriplem2  15360  pythagtrip  15377  pceu  15389  pcprmpw2  15424  unbenlem  15450  4sqlem12  15498  vdwapval  15515  vdwapun  15516  vdwmc2  15521  vdwpc  15522  vdwlem2  15524  vdwlem10  15532  vdwlem13  15535  vdwnnlem1  15537  rami  15557  cshwsiun  15644  cshwrepswhash1  15647  brssc  16297  isdrs  16757  drsdir  16758  drsdirfi  16761  isdrs2  16762  ipodrsima  16988  gsumvalx  17093  gsumpropd  17095  gsumress  17099  isnsgrp  17111  sgrp2nmndlem5  17239  grpinvex  17255  dfgrp2  17270  grpidinv2  17297  grpidinv  17298  dfgrp3lem  17336  grp1  17345  imasgrp2  17353  conjnmzb  17518  gaorb  17563  orbsta  17569  symgfix2  17659  symgextfo  17665  pmtrprfvalrn  17731  psgnunilem3  17739  psgneu  17749  psgnval  17750  psgnvali  17751  psgnvalii  17752  ispgp  17830  subgpgp  17835  sylow1  17841  pgpfi  17843  sylow2blem3  17860  fislw  17863  sylow3lem2  17866  lsmelvalm  17889  lsmass  17906  pj1fval  17930  pj1val  17931  pj1eu  17932  pj1id  17935  efgrelexlema  17985  efgrelexlemb  17986  efgredeu  17988  cyggeninv  18108  cygabl  18115  pgpfac1lem2  18297  pgpfac1lem3  18299  pgpfac1lem4  18300  pgpfac1  18302  pgpfaclem2  18304  pgpfac  18306  dvdsrval  18468  dvdsr  18469  subrgdvds  18617  lss1d  18784  lspsn  18823  lspsnel  18824  lspsolvlem  18963  rspsn  19075  opsrval  19295  znf1o  19719  cygznlem3  19737  psgndiflemA  19766  ellspd  19960  mat1dimelbas  20096  mat1dimbas  20097  scmatval  20129  scmatel  20130  scmateALT  20137  mat0scmat  20163  decpmataa0  20392  decpmatmulsumfsupp  20397  pmatcollpw2lem  20401  pm2mpmhmlem1  20442  chpscmat  20466  basis2  20566  eltg2  20573  tg2  20580  isclo  20701  neival  20716  isnei  20717  isneip  20719  restbas  20772  neitr  20794  cnpval  20850  iscnp  20851  cnpimaex  20870  lmbr  20872  lmbr2  20873  cnprest2  20904  lmff  20915  regsep  20948  pnrmopn  20957  nrmsep3  20969  isnrm2  20972  iscmp  21001  cmpsublem  21012  cmpsub  21013  tgcmp  21014  sscmp  21018  hauscmplem  21019  1stcclb  21057  1stcfb  21058  is2ndc  21059  2ndc1stc  21064  1stcrest  21066  2ndcctbss  21068  1stcelcls  21074  llyeq  21083  nllyeq  21084  hausllycmp  21107  lly1stc  21109  refssex  21124  refun0  21128  islocfin  21130  locfinnei  21136  comppfsc  21145  txbas  21180  ptval  21183  ptpjopn  21225  ptclsg  21228  txcnp  21233  ptcnp  21235  txrest  21244  ptrescn  21252  txcmp  21256  tx1stc  21263  xkococn  21273  kqreglem1  21354  fbasssin  21450  fbssfi  21451  fbssint  21452  fbun  21454  fgss2  21488  fgcl  21492  ufli  21528  fmfnfmlem3  21570  fbflim2  21591  hauspwpwf1  21601  flfneii  21606  flftg  21610  txflf  21620  fclscf  21639  alexsubb  21660  alexsubALT  21665  tsmssubm  21756  ustincl  21821  ustdiag  21822  ustinvel  21823  ustexhalf  21824  ust0  21833  trust  21843  elutop  21847  ucnval  21891  ucncn  21899  cfiluexsm  21904  cfiluweak  21909  blssps  22039  blss  22040  imasf1oxms  22104  mopni  22107  metss  22123  metrest  22139  metcnp3  22155  cfilucfil  22174  metuel2  22180  nlmvscn  22301  nrginvrcn  22306  icccmplem1  22433  icccmplem2  22434  icccmp  22436  divcn  22479  cncfval  22499  elcncf2  22501  cncfmet  22519  cnheibor  22562  evth  22566  lebnumlem3  22570  lebnum  22571  xlebnum  22572  lebnumii  22573  ipcn  22853  lmmbr  22864  lmmbr2  22865  cfilfval  22870  cfili  22874  iscfil3  22879  caufval  22881  iscau  22882  iscau2  22883  equivcfil  22905  equivcau  22906  lmcau  22919  ovolval  23049  elovolm  23050  ovolgelb  23055  ovoliunlem1  23077  ovoliun2  23081  ovolshftlem1  23084  ovolscalem1  23088  ovolicc  23098  ioombl1lem4  23136  uniioombllem2  23157  mbfaddlem  23233  mbfsup  23237  mbfinf  23238  mbflimsup  23239  i1fmulc  23276  itg1climres  23287  itg2val  23301  itg2l  23302  itg2leub  23307  itg2seq  23315  itg2monolem1  23323  itg2mono  23326  itg2i1fseq2  23329  cniccibl  23413  ellimc3  23449  limciun  23464  dvferm1  23552  dvferm2  23554  lhop1lem  23580  ply1divex  23700  ig1peu  23735  plyval  23753  elply2  23756  coeval  23783  coeeu  23785  coelem  23786  coeeq  23787  plydivlem4  23855  plydivex  23856  aannenlem2  23888  aalioulem2  23892  aaliou2  23899  ulmval  23938  ulm2  23943  ulmcau  23953  ulmdvlem3  23960  abelthlem9  23998  abelth  23999  efif1olem4  24095  eflogeq  24152  efopn  24204  cxpcn3  24289  cxpeq  24298  rlimcnp  24492  lgamgulmlem6  24560  muval  24658  dchrptlem1  24789  dchrptlem2  24790  lgsdchrval  24879  2lgslem1b  24917  pntpbnd  25077  pntibndlem3  25081  pntibnd  25082  pntlemi  25093  pntleme  25097  pntlemp  25099  pnt3  25101  istrkgld  25158  istrkg3ld  25160  axtgsegcon  25163  axtgpasch  25166  axtgcont1  25167  axtgupdim2  25170  legov  25280  islnopp  25431  ishpg  25451  hpgbr  25452  hpgcom  25459  iscgra  25501  iscgra1  25502  isinag  25529  isleag  25533  ttgval  25555  ttgitvval  25562  ttgelitv  25563  brbtwn  25579  brcgr  25580  axpasch  25621  axlowdim2  25640  axlowdim  25641  axcontlem2  25645  axcontlem4  25647  axcontlem7  25650  axcontlem8  25651  upgredg2vtx  25814  nbgraf1olem1  25970  cusgrafilem2  26008  cusgrafi  26010  wwlkn0  26217  clwwlknscsh  26347  erclwwlkneq  26351  eleclclwwlkn  26360  hashecclwwlkn1  26361  usghashecclwwlk  26362  el2wlksot  26407  el2pthsot  26408  2spot2iun2spont  26418  iseupa  26492  3cyclfrgrarn1  26539  usgn0fidegnn0  26556  frgrancvvdeqlem4  26560  friendshipgt3  26648  isgrpo  26735  isgrpoi  26736  grpoidinvlem3  26744  grpoideu  26747  grpoidinv2  26753  nmoofval  27001  nmooval  27002  nmosetn0  27004  nmoolb  27010  nmoubi  27011  nmlno0lem  27032  chcompl  27483  pjhthmo  27545  pjhval  27640  pjpreeq  27641  h1de2ci  27799  elspansn  27809  nmopval  28099  nmopsetn0  28108  nmfnval  28119  nmfnsetn0  28121  eigvecval  28139  hhcno  28147  hhcnf  28148  nmoplb  28150  nmopub  28151  nmfnlb  28167  nmfnleub  28168  eleigvec  28200  nmlnop0iALT  28238  nmopun  28257  nmcexi  28269  branmfn  28348  pjnmopi  28391  cvbr  28525  hatomic  28603  chrelat2  28613  cdjreui  28675  cdj3lem2  28678  reuxfr4d  28714  elabreximd  28732  br8d  28802  unipreima  28826  abfmpunirn  28832  curry2ima  28869  toslublem  28998  tosglblem  29000  archirng  29073  archiexdiv  29075  archiabllem2a  29079  archiabl  29083  isarchiofld  29148  crefi  29242  pcmplfin  29255  pstmfval  29267  tpr2rico  29286  rge0scvg  29323  ismntop  29398  esumc  29440  esumpcvgval  29467  esum2dlem  29481  inelsros  29568  diffiunisros  29569  dya2icoseg2  29667  dya2iocuni  29672  eulerpartlemgvv  29765  eulerpartlemgh  29767  bnj66  30184  bnj873  30248  bnj18eq1  30251  bnj1234  30335  bnj1318  30347  subfacp1lem3  30418  pconcn  30460  cnpcon  30466  txpcon  30468  conpcon  30471  iscvm  30495  cvmcov  30499  cvmopnlem  30514  cvmliftlem15  30534  cvmlift3lem2  30556  cvmlift3lem4  30558  cvmlift3  30564  br8  30899  br6  30900  br4  30901  dfrdg2  30945  dfrdg3  30946  orderseqlem  30993  poseq  30994  soseq  30995  elno  31043  sltval  31044  nobndlem6  31096  nofulllem1  31101  nofulllem2  31102  nofulllem5  31105  altxpeq2  31251  funtransport  31308  fvtransport  31309  brcolinear2  31335  colineardim1  31338  segcon2  31382  brsegle  31385  funray  31417  fvray  31418  funline  31419  linedegen  31420  fvline  31421  ellines  31429  gtinfOLD  31484  nn0prpwlem  31487  fnessref  31522  neibastop2lem  31525  neibastop2  31526  tailfb  31542  unblimceq0lem  31667  unblimceq0  31668  unbdqndv2  31672  bj-finsumval0  32324  relowlssretop  32387  phpreu  32563  matunitlindflem2  32576  ptrest  32578  poimirlem4  32583  poimirlem17  32596  poimirlem20  32599  poimirlem24  32603  poimirlem26  32605  poimirlem27  32606  poimirlem28  32607  poimirlem31  32610  poimirlem32  32611  poimir  32612  heicant  32614  mblfinlem1  32616  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  itg2addnclem  32631  itg2addnclem3  32633  itg2addnc  32634  itg2gt0cn  32635  cnicciblnc  32651  ftc1anclem6  32660  unirep  32677  indexa  32698  sdclem2  32708  sdclem1  32709  sdc  32710  fdc  32711  fdc1  32712  incsequz  32714  istotbnd  32738  sstotbnd2  32743  equivtotbnd  32747  isbnd  32749  bndss  32755  ssbnd  32757  totbndbnd  32758  ismtybndlem  32775  heibor1lem  32778  heiborlem1  32780  heiborlem6  32785  heiborlem8  32787  heiborlem10  32789  heibor  32790  rngoid  32871  isgrpda  32924  isdrngo2  32927  divrngidl  32997  prnc  33036  isfldidl  33037  prtlem5  33162  prtlem13  33171  prtlem16  33172  islshp  33284  lsmsat  33313  lcvbr  33326  lsatcv0  33336  lshpsmreu  33414  lshpkrlem1  33415  lshpkrlem2  33416  lshpkrlem3  33417  lshpkrcl  33421  lshpset2N  33424  islshpkrN  33425  cvrval  33574  atlex  33621  glbconxN  33682  hlsuprexch  33685  islln  33810  islpln  33834  islpln5  33839  lvolex3N  33842  islvol  33877  islvol5  33883  ispointN  34046  pmapglbx  34073  paddval  34102  elpaddn0  34104  elpaddat  34108  elpadd0  34113  4atex  34380  4atex2  34381  cdlemefrs29bpre1  34703  cdlemefrs32fva  34706  cdlemg33b  35013  dvhb1dimN  35292  dvhopellsm  35424  dib1dim  35472  diclspsn  35501  dihglblem2aN  35600  dihglblem2N  35601  dih1dimatlem  35636  dvh3dimatN  35746  dvh2dim  35752  dvh3dim  35753  dvh4dimN  35754  dvh3dim3N  35756  dochfl1  35783  lcfl7N  35808  lcf1o  35858  lcfrlem39  35888  mapdpglem3  35982  hvmapvalvalN  36068  hdmap14lem2a  36177  hdmapglem7a  36237  elrfi  36275  isnacs  36285  nacsfg  36286  nacsfix  36293  mzpcompact2lem  36332  eldiophb  36338  eldioph  36339  eldioph2  36343  eldioph2b  36344  eldioph3  36347  eldiophss  36356  diophrex  36357  sbcrexgOLD  36367  sbc2rexgOLD  36370  rexrabdioph  36376  rexfrabdioph  36377  elnn0rabdioph  36385  dvdsrabdioph  36392  eldioph4b  36393  eldioph4i  36394  diophren  36395  rencldnfilem  36402  pell1234qrdich  36443  jm2.27  36593  expdiophlem1  36606  wepwsolem  36630  aomclem8  36649  islnr3  36704  lnr2i  36705  lpirlnr  36706  hbtlem1  36712  hbtlem2  36713  hbtlem7  36714  hbtlem4  36715  hbtlem5  36717  hbtlem6  36718  dgraaval  36733  dgraalem  36734  dgraaub  36737  rngunsnply  36762  brtrclfv2  37038  clsk1indlem1  37363  extoimad  37486  elabrexg  38229  foelrnf  38368  disjrnmpt2  38370  upbdrech  38460  ssfiunibd  38464  supxrgere  38490  supxrgelem  38494  supxrge  38495  suplesup  38496  infxr  38524  infleinf  38529  iccshift  38591  iooshift  38595  climinf  38673  climinff  38678  ellimcabssub0  38684  climf  38689  limcperiod  38695  limclner  38718  climf2  38733  clim2d  38740  cncfshiftioo  38778  fperdvper  38808  itgiccshift  38872  itgperiod  38873  stoweidlem27  38920  stoweidlem31  38924  stoweidlem43  38936  stoweidlem46  38939  stoweidlem52  38945  stoweidlem60  38953  fourierdlem42  39042  fourierdlem48  39047  fourierdlem51  39050  fourierdlem54  39053  fourierdlem63  39062  fourierdlem64  39063  fourierdlem65  39064  fourierdlem68  39067  fourierdlem70  39069  fourierdlem71  39070  fourierdlem73  39072  fourierdlem80  39079  fourierdlem81  39080  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem92  39091  fourierdlem96  39095  fourierdlem97  39096  fourierdlem98  39097  fourierdlem99  39098  fourierdlem100  39099  fourierdlem103  39102  fourierdlem104  39103  fourierdlem105  39104  fourierdlem108  39107  fourierdlem109  39108  fourierdlem110  39109  fourierdlem112  39111  fourierdlem113  39112  sge0pnffigt  39289  sge0resplit  39299  ovnval2  39435  ovnval2b  39442  ovnlecvr  39448  ovnpnfelsup  39449  ovn0lem  39455  ovnsubaddlem1  39460  hoidmvlelem1  39485  ovnhoilem1  39491  ovnhoi  39493  ovnlecvr2  39500  hoiqssbl  39515  ovolval5lem2  39543  ovolval5lem3  39544  ovolval5  39545  ovnovol  39549  cbvrex2  39822  afvelrnb  39892  afvelrnb0  39893  iccelpart  39971  iccpartiun  39972  icceuelpart  39974  fmtnofac2lem  40018  fmtnofac2  40019  fmtnofac1  40020  m1expevenALTV  40098  odd2np1ALTV  40123  opoeALTV  40132  opeoALTV  40133  isgbo  40174  isgboa  40175  7gbo  40194  9gboa  40196  11gboa  40197  bgoldbwt  40199  nnsum3primesgbe  40208  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  bgoldbtbnd  40225  cshword2  40300  usgredg4  40444  ushgredgedga  40456  ushgredgedgaloop  40458  dfnbgr2  40561  nbgrel  40564  nbumgrvtx  40568  nbgrnself  40583  uvtxael1  40622  uvtxa01vtx0  40623  cusgrfilem2  40672  cusgrfi  40674  vtxd0nedgb  40703  fusgrn0degnn0  40714  wlkOnl1iedg  40873  wspniunwspnon  41130  elwwlks2on  41162  clwwlksnscsh  41247  erclwwlksneq  41251  eleclclwwlksn  41260  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  3cyclfrgrrn1  41455  frgrncvvdeqlem4  41472  av-friendshipgt3  41552  0nodd  41600  1odd  41601  2nodd  41602  0even  41721  1neven  41722  2even  41723  2zlidl  41724  2zrngamgm  41729  2zrngagrp  41733  2zrngmmgm  41736  2zrngnmrid  41740  lcoval  41995  el0ldep  42049  ldepspr  42056  zlmodzxzldep  42087
  Copyright terms: Public domain W3C validator