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

Theorem ralbidv 2563
Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.)
Hypothesis
Ref Expression
ralbidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
ralbidv  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)

Proof of Theorem ralbidv
StepHypRef Expression
1 nfv 1605 . 2  |-  F/ x ph
2 ralbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2ralbid 2561 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wral 2543
This theorem is referenced by:  ralbii  2567  2ralbidv  2585  rexralbidv  2587  raleqbi1dv  2744  raleqbidv  2748  cbvral2v  2772  rspc2  2889  rspc3v  2893  reu6i  2956  reu7  2960  sbcralt  3063  sbcralg  3065  raaan  3561  raaanv  3562  r19.12sn  3696  2ralunsn  3816  elintg  3870  elintrabg  3875  eliin  3910  disjprg  4019  disjxun  4021  poeq1  4317  somo  4348  frirr  4370  fr2nr  4371  frminex  4373  wereu2  4390  reusv2lem2  4536  reusv3  4542  reusv6OLD  4545  fr3nr  4571  onssmin  4588  posn  4758  frsn  4760  ralxpf  4830  cnvpo  5213  funcnvuni  5317  iinpreima  5655  dff4  5674  dff13f  5784  f1oweALT  5851  ofreq  6081  frxp  6225  sorpssuni  6286  sorpssint  6287  eusvobj2  6337  riotasvd  6347  smoeq  6367  recseq  6389  tfrlem3  6393  tfrlem3a  6394  tfrlem12  6405  tz7.48lem  6453  elixp2  6820  undifixp  6852  xpf1o  7023  nneneq  7044  ac6sfi  7101  frfi  7102  fipreima  7161  indexfi  7163  marypha1lem  7186  marypha1  7187  supeq1  7198  supmo  7203  eqsup  7207  supub  7210  suplub  7211  supmaxlem  7215  supisoex  7222  oieq1  7227  ordtypecbv  7232  ordtypelem3  7235  ordtypelem6  7238  ordtypelem7  7239  ordtypelem9  7241  wemaplem1  7261  wemaplem2  7262  zfregcl  7308  oemapval  7385  oemapvali  7386  cantnf  7395  wemapwe  7400  rankval3b  7498  unbndrank  7514  rankunb  7522  rankuni2b  7525  tcrank  7554  scottex  7555  scottexs  7557  scott0s  7558  bnd2  7563  dfac8clem  7659  ac5num  7663  acni  7672  acni2  7673  alephval3  7737  dfac4  7749  dfac5lem5  7754  dfac5  7755  dfac2a  7756  dfac2  7757  dfacacn  7767  kmlem2  7777  kmlem13  7788  cflem  7872  cflecard  7879  cfeq0  7882  cfsuc  7883  cfflb  7885  cofsmo  7895  cfsmolem  7896  cfcoflem  7898  coftr  7899  alephsing  7902  fin23lem11  7943  isfin3ds  7955  fin23lem17  7964  fin23lem39  7976  isf33lem  7992  isf34lem6  8006  fin1a2lem13  8038  hsmexlem4  8055  hsmex  8058  axcc2lem  8062  axcc3  8064  dcomex  8073  axdc2lem  8074  axdc3lem2  8077  axdc3lem3  8078  axdc3  8080  axdc4lem  8081  axcclem  8083  zorn2lem2  8124  zorn2lem7  8129  zorn2g  8130  zornn0g  8132  ttukeylem7  8142  axdclem2  8147  brdom3  8153  brdom7disj  8156  brdom6disj  8157  alephval2  8194  inar1  8397  axgroth6  8450  pinq  8551  nqereu  8553  prlem934  8657  supexpr  8678  supsrlem  8733  axpre-sup  8791  fimaxre2  9702  lbreu  9704  lbinfm  9707  sup2  9710  infm3  9713  supmul1  9719  supmullem2  9721  supmul  9722  infmrcl  9733  nnsub  9784  uzwo  10281  uzwoOLD  10282  nnwof  10285  uzinfmi  10297  ublbneg  10302  lbzbi  10306  zsupss  10307  uzsupss  10310  uzwo3  10311  zmax  10313  rpnnen1lem1  10342  rpnnen1lem2  10343  rpnnen1lem3  10344  rpnnen1lem4  10345  rpnnen1lem5  10346  xrsupsslem  10625  xrinfmsslem  10626  xrsupss  10627  xrinfmss  10628  iccsupr  10736  flval2  10944  flval3  10945  fsequb  11037  axdc4uzlem  11044  faclbnd4lem4  11309  bccl  11334  hashbc  11391  wrdind  11477  sqrlem3  11730  rexanre  11830  rexico  11837  cau4  11840  caubnd2  11841  caubnd  11842  clim  11968  rlim  11969  rlim2  11970  rlim2lt  11971  rlim3  11972  clim2  11978  clim2c  11979  clim0c  11981  rlim0  11982  rlim0lt  11983  ello12r  11991  ello1d  11997  lo1bdd2  11998  lo1bddrp  11999  elo12r  12002  rlimconst  12018  rlimresb  12039  rlimcld2  12052  climabs0  12059  rlimcn2  12064  reccn2  12070  cn1lem  12071  rlimo1  12090  o1rlimmul  12092  lo1add  12100  lo1mul  12101  isercoll  12141  caucvgrlem  12145  incexclem  12295  climcnds  12310  divrcnv  12311  ruclem12  12519  sqr2irr  12527  gcdcllem1  12690  gcdcllem2  12691  maxprmfct  12792  pc2dvds  12931  pcz  12933  prmpwdvds  12951  infpn2  12960  prmreclem1  12963  prmreclem2  12964  prmreclem3  12965  prmreclem5  12967  prmreclem6  12968  vdwlem6  13033  vdwlem8  13035  vdwlem13  13040  vdwnnlem1  13042  vdwnn  13045  ramz  13072  ramcl  13076  prdsleval  13376  imasval  13414  imasaddfnlem  13430  imasvscafn  13439  mrisval  13532  isacs  13553  isacs2  13555  isacs1i  13559  mreacs  13560  acsfn  13561  acsfn2  13565  catideu  13577  comfeq  13609  catpropd  13612  isnat  13821  isprs  14064  drsdirfi  14072  ispos  14081  lubfval  14112  lubval  14113  lubprop  14114  lubid  14116  glbfval  14117  glbval  14118  glbprop  14119  joinval2  14123  joinlem  14124  meetval2  14130  meetlem  14131  isglbd  14221  lubl  14224  lubun  14227  clatleglb  14230  poslubmo  14250  poslubd  14251  ipodrsima  14268  isdlat  14296  spwval2  14333  spwmo  14335  spwpr2  14337  spwpr4  14340  mgmidmo  14370  ismgmid  14387  ismgmid2  14390  ismndd  14396  mhmima  14440  gsumvallem1  14448  gsumvallem2  14449  gsumvalx  14451  gsumress  14454  gsumval2  14460  gsumwspan  14468  isgrpinv  14532  issubg4  14638  0subg  14642  cycsubgcl  14643  isnsg2  14647  nsgacs  14653  elnmz  14656  ghmrn  14696  ghmnsgima  14706  isga  14745  orbsta  14767  cntzfval  14796  elcntz  14798  resscntz  14807  oppgsubg  14836  odeq  14865  gexid  14892  gexlem2  14893  gexdvds  14895  isslw  14919  pgpssslw  14925  sylow2alem1  14928  sylow2alem2  14929  efgval  15026  efgrelexlemb  15059  efgcpbllemb  15064  gexex  15145  dmdprd  15236  dprd2da  15277  pgpfac1lem5  15314  isabv  15584  islss  15692  lssacs  15724  reslmhm  15809  islbs  15829  pj1lmhm  15853  lbsacsbs  15909  isrrg  16029  opsrval  16216  zlpir  16444  ocvfval  16566  elocv  16568  iunocv  16581  basgen2  16727  bastop1  16731  isclo  16824  ordtbaslem  16918  iscn  16965  cnpval  16966  iscnp  16967  iscnp3  16974  lmbr  16988  lmbr2  16989  lmbrf  16990  cnprest  17017  cnprest2  17018  t0sep  17052  isreg  17060  t1sep2  17097  tgcmp  17128  1stcclb  17170  1stcfb  17171  2ndc1stc  17177  1stcrest  17179  2ndcdisj  17182  islly  17194  isnlly  17195  lly1stc  17222  elkgen  17231  kgencn  17251  elpt  17267  elptr  17268  ptcnplem  17315  tx1stc  17344  cnmpt21  17365  kqt0lem  17427  isr0  17428  regr1lem2  17431  r0sep  17439  nrmr0reg  17440  flffbas  17690  cnflf  17697  cnflf2  17698  lmflf  17700  txflf  17701  fclsopni  17710  fclsnei  17714  fclsrest  17719  fcfnei  17730  cnfcf  17737  alexsubb  17740  alexsubALTlem3  17743  divstgplem  17803  tsmsfbas  17810  tsmsgsum  17821  tsmsres  17826  tsmsf1o  17827  tsmsxplem1  17835  tsmsxp  17837  ismet  17888  isxmet  17889  imasdsf1olem  17937  imasf1oxmet  17939  imasf1omet  17940  metss  18054  met1stc  18067  prdsxmslem2  18075  metcnpi3  18092  txmetcnp  18093  nlmvscn  18198  nrginvrcnlem  18201  nmoval  18224  nmolb  18226  nghmcn  18254  qtopbaslem  18267  icccmplem2  18328  icccmplem3  18329  reconnlem2  18332  metdscn  18360  cncfval  18392  elcncf2  18394  elcncf1di  18399  mulc1cncf  18409  cncfmet  18412  cnllycmp  18454  evth  18457  lebnumlem3  18461  lebnum  18462  xlebnum  18463  ishtpy  18470  isphtpy  18479  pi1xfr  18553  pi1coghm  18559  ipcn  18673  lmmbr2  18685  lmmbr3  18686  lmmbrf  18688  cfilfval  18690  iscfil  18691  fmcfil  18698  caufval  18701  iscau  18702  iscau2  18703  iscau3  18704  iscau4  18705  iscauf  18706  caucfil  18709  cfilresi  18721  causs  18724  lmclim  18728  cncmet  18744  minveclem4c  18789  minveclem2  18790  minveclem3b  18792  minveclem4  18796  minveclem6  18798  minveclem7  18799  ivthlem2  18812  ivthlem3  18813  cniccbdd  18821  ovolunlem1  18856  ovoliunlem1  18861  ovoliun2  18865  ovolicc2lem3  18878  ismbl  18885  ioombl1lem4  18918  uniioombllem2  18938  uniioombllem6  18943  dyadmax  18953  dyadmbllem  18954  dyadmbl  18955  opnmbllem  18956  volcn  18961  ismbf1  18981  ismbf  18985  mbfeqalem  18997  mbfinf  19020  mbflimsup  19021  itg1climres  19069  mbfi1fseqlem6  19075  mbfi1flimlem  19077  itg2seq  19097  itg2monolem1  19105  itg2i1fseq  19110  itg2i1fseq2  19111  itg2cnlem1  19116  itg2cnlem2  19117  isibl  19120  dveflem  19326  ply1divex  19522  fta1g  19553  plyeq0lem  19592  dgrco  19656  plydivex  19677  fta1  19688  vieta1  19692  aannenlem1  19708  aannenlem2  19709  aalioulem2  19713  aalioulem3  19714  ulmval  19759  ulm2  19764  ulmi  19765  ulmres  19767  ulmshftlem  19768  ulmcaulem  19771  ulmcau  19772  ulmss  19774  ulmbdd  19775  ulmdvlem1  19777  ulmdvlem3  19779  iblulm  19783  abelthlem8  19815  pilem2  19828  pilem3  19829  divlogrlim  19982  cxpcn3  20088  dmarea  20252  rlimcnp  20260  cxplim  20266  cxploglim  20272  scvxcvx  20280  emcllem6  20294  ftalem1  20310  ftalem2  20311  ftalem3  20312  isppw2  20353  perfectlem2  20469  2sqlem6  20608  2sqlem10  20613  dchrisumlema  20637  dchrisumlem2  20639  dchrisumlem3  20640  dchrisum0  20669  pntpbnd  20737  pntibndlem3  20741  pntibnd  20742  pntleme  20757  pntlem3  20758  pntlemp  20759  pnt3  20761  isgrpo  20863  isgrpo2  20864  isgrpoi  20865  grpoideu  20876  grpoidinv2  20885  isgrp2d  20902  isgrpda  20964  exidu1  20993  cmpidelt  20996  cnid  21018  mulid  21023  ghgrp  21035  isrngod  21046  rngoideu  21051  cnrngo  21070  vci  21104  isvclem  21133  isnvlem  21166  nvi  21170  nmcvcn  21268  lnoval  21330  islno  21331  isblo3i  21379  blo3i  21380  blocnilem  21382  blocni  21383  ajfval  21387  ubthlem1  21449  ubthlem2  21450  ubthlem3  21451  ubth  21452  minvecolem2  21454  minvecolem3  21455  minvecolem4c  21458  minvecolem4  21459  minvecolem5  21460  minvecolem6  21461  minvecolem7  21462  htthlem  21497  h2hcau  21559  h2hlm  21560  hilid  21740  hcau  21763  hlimi  21767  hlim2  21771  ocel  21860  adjsym  22413  ellnop  22438  ellnfn  22463  hhcno  22484  hhcnf  22485  0cnop  22559  0cnfn  22560  idcnop  22561  lnopeq  22589  elunop2  22593  lnophm  22599  lnconi  22613  lnopcnbd  22616  lnfncnbd  22637  imaelshi  22638  riesz3i  22642  riesz4i  22643  riesz4  22644  riesz1  22645  cnlnadjlem2  22648  cnlnadjlem5  22651  cnlnadjlem8  22654  cnlnadji  22656  nmopadjlei  22668  cnvbraval  22690  leopg  22702  leoppos  22706  mdbr  22874  dmdbr  22879  cdj3i  23021  ballotleme  23055  funcnv5mpt  23236  rge0scvg  23373  esumpcvgval  23446  isrnmeas  23531  ismbfm  23557  isanmbfm  23561  mbfmcst  23564  derangenlem  23702  subfacp1lem3  23713  subfacp1lem5  23715  subfacp1lem6  23716  subfacp1  23717  erdszelem8  23729  kur14  23747  cnpcon  23761  rescon  23777  cvmscbv  23789  iscvm  23790  cvmsi  23796  cvmsval  23797  cvmlift3lem2  23851  iseupa  23881  snmlval  23914  ghomgrpilem1  23992  dedekind  24082  dedekindle  24083  dfpo2  24112  dfon2lem9  24147  dfrdg2  24152  dfrdg3  24153  poseq  24253  soseq  24254  wfrlem1  24256  wfrlem15  24270  frrlem1  24281  sltval  24301  nocvxminlem  24344  nobndlem2  24347  nobndlem8  24353  nobndup  24354  nobnddown  24355  brbtwn2  24533  colinearalg  24538  axsegconlem1  24545  axsegcon  24555  ax5seglem4  24560  ax5seglem5  24561  axlowdim  24589  axeuclidlem  24590  axcontlem1  24592  axcontlem2  24593  axcontlem4  24595  axcontlem5  24596  axcontlem8  24599  axcontlem12  24603  bpolylem  24783  bpolyval  24784  elixp2b  25154  prjmapcp2  25170  islatalg  25183  ubos  25256  puub2  25258  puub  25259  supdef  25262  ismxl2  25267  ismnl2  25268  defge3  25271  defse3  25272  clfsebsr  25349  idlvalNEW  25445  isidlNEW  25446  vecval1b  25451  vecval3b  25452  vri  25492  basexre  25522  usptoplem  25546  istopx  25547  usptop  25550  prcnt  25551  cnfilca  25556  flfnei2  25577  tcnvec  25690  isded  25736  dedi  25737  iscatOLD  25754  cati  25755  isfunb  25835  isntr  25873  islimcat  25876  indcls2  25996  pfsubkl  26047  isibg2  26110  isibg2aa  26112  isibg2aalem1  26113  isibg2aalem2  26114  bsstrs  26146  nbssntrs  26147  isibcg  26191  nn0prpwlem  26238  isfne  26268  isfne4  26269  isfne2  26271  isfne3  26272  isref  26279  islocfin  26296  neibastop3  26311  topmeet  26313  topjoin  26314  filnetlem4  26330  f1opr  26391  upixp  26403  indexdom  26413  filbcmb  26432  sdclem2  26452  fdc  26455  lmclim2  26474  caures  26476  istotbnd  26493  istotbnd3  26495  sstotbnd  26499  isbnd  26504  heibor  26545  bfp  26548  rrncmslem  26556  exidres  26568  exidresid  26569  idlval  26638  isidl  26639  0idl  26650  unichnidl  26656  pridl  26662  ismaxidl  26665  smprngopr  26677  igenval2  26691  prnc  26692  ispridlc  26695  isnacs  26779  isnacs2  26781  nacsfix  26787  mzpclval  26803  elmzpcl  26804  rencldnfilem  26903  infmrgelbi  26963  pellfundre  26966  pellfundlb  26969  wepwsolem  27138  fnwe2lem2  27148  aomclem8  27159  dfac11  27160  frlmlbs  27249  gicabl  27263  islindf  27282  islinds2  27283  islindf2  27284  lindfrn  27291  lsslindf  27300  islindf4  27308  islnr3  27319  hbtlem2  27328  hbtlem5  27332  psgnunilem2  27418  psgnunilem3  27419  ubelsupr  27691  evthf  27698  fnchoice  27700  stoweidlem5  27754  stoweidlem9  27758  stoweidlem15  27764  stoweidlem16  27765  stoweidlem27  27776  stoweidlem28  27777  stoweidlem31  27780  stoweidlem34  27783  stoweidlem37  27786  stoweidlem46  27795  stoweidlem48  27797  stoweidlem51  27800  stoweidlem52  27801  stoweidlem59  27808  wallispilem3  27816  stirlinglem13  27835  cbvral2  27950  raaan2  27953  2reu4a  27967  dfdfat2  27994  bnj1185  28826  bnj1385  28865  bnj66  28892  bnj106  28900  bnj155  28911  bnj852  28953  bnj893  28960  bnj1228  29041  bnj1234  29043  bnj1463  29085  lubunNEW  29163  islfl  29250  eqlkr  29289  eqlkr3  29291  glbconN  29566  hlsuprexch  29570  ispsubsp  29934  ldilset  30298  isldil  30299  dilsetN  30342  isdilN  30343  trlset  30350  trlval  30351  cdleme27b  30557  cdleme29b  30564  cdleme31so  30568  cdleme31sn1  30570  cdleme31sn1c  30577  cdleme31fv  30579  cdleme40v  30658  istendo  30949  cdlemkid3N  31122  cdlemkid4  31123  cdlemkid5  31124  dihfval  31421  dihval  31422  islpolN  31673  hdmapffval  32019  hdmapfval  32020  hdmapval  32021  hdmapval2lem  32024  hgmapffval  32078  hgmapfval  32079  hgmapval  32080  hgmapvs  32084
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1532  df-ral 2548
  Copyright terms: Public domain W3C validator