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

Theorem ralbidv 2576
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 1609 . 2  |-  F/ x ph
2 ralbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2ralbid 2574 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 2556
This theorem is referenced by:  ralbii  2580  2ralbidv  2598  rexralbidv  2600  raleqbi1dv  2757  raleqbidv  2761  cbvral2v  2785  rspc2  2902  rspc3v  2906  reu6i  2969  reu7  2973  sbcralt  3076  sbcralg  3078  raaan  3574  raaanv  3575  r19.12sn  3709  2ralunsn  3832  elintg  3886  elintrabg  3891  eliin  3926  disjprg  4035  disjxun  4037  poeq1  4333  somo  4364  frirr  4386  fr2nr  4387  frminex  4389  wereu2  4406  reusv2lem2  4552  reusv3  4558  reusv6OLD  4561  fr3nr  4587  onssmin  4604  posn  4774  frsn  4776  ralxpf  4846  cnvpo  5229  funcnvuni  5333  iinpreima  5671  dff4  5690  dff13f  5800  f1oweALT  5867  ofreq  6097  frxp  6241  sorpssuni  6302  sorpssint  6303  eusvobj2  6353  riotasvd  6363  smoeq  6383  recseq  6405  tfrlem3  6409  tfrlem3a  6410  tfrlem12  6421  tz7.48lem  6469  elixp2  6836  undifixp  6868  xpf1o  7039  nneneq  7060  ac6sfi  7117  frfi  7118  fipreima  7177  indexfi  7179  marypha1lem  7202  marypha1  7203  supeq1  7214  supmo  7219  eqsup  7223  supub  7226  suplub  7227  supmaxlem  7231  supisoex  7238  oieq1  7243  ordtypecbv  7248  ordtypelem3  7251  ordtypelem6  7254  ordtypelem7  7255  ordtypelem9  7257  wemaplem1  7277  wemaplem2  7278  zfregcl  7324  oemapval  7401  oemapvali  7402  cantnf  7411  wemapwe  7416  rankval3b  7514  unbndrank  7530  rankunb  7538  rankuni2b  7541  tcrank  7570  scottex  7571  scottexs  7573  scott0s  7574  bnd2  7579  dfac8clem  7675  ac5num  7679  acni  7688  acni2  7689  alephval3  7753  dfac4  7765  dfac5lem5  7770  dfac5  7771  dfac2a  7772  dfac2  7773  dfacacn  7783  kmlem2  7793  kmlem13  7804  cflem  7888  cflecard  7895  cfeq0  7898  cfsuc  7899  cfflb  7901  cofsmo  7911  cfsmolem  7912  cfcoflem  7914  coftr  7915  alephsing  7918  fin23lem11  7959  isfin3ds  7971  fin23lem17  7980  fin23lem39  7992  isf33lem  8008  isf34lem6  8022  fin1a2lem13  8054  hsmexlem4  8071  hsmex  8074  axcc2lem  8078  axcc3  8080  dcomex  8089  axdc2lem  8090  axdc3lem2  8093  axdc3lem3  8094  axdc3  8096  axdc4lem  8097  axcclem  8099  zorn2lem2  8140  zorn2lem7  8145  zorn2g  8146  zornn0g  8148  ttukeylem7  8158  axdclem2  8163  brdom3  8169  brdom7disj  8172  brdom6disj  8173  alephval2  8210  inar1  8413  axgroth6  8466  pinq  8567  nqereu  8569  prlem934  8673  supexpr  8694  supsrlem  8749  axpre-sup  8807  fimaxre2  9718  lbreu  9720  lbinfm  9723  sup2  9726  infm3  9729  supmul1  9735  supmullem2  9737  supmul  9738  infmrcl  9749  nnsub  9800  uzwo  10297  uzwoOLD  10298  nnwof  10301  uzinfmi  10313  ublbneg  10318  lbzbi  10322  zsupss  10323  uzsupss  10326  uzwo3  10327  zmax  10329  rpnnen1lem1  10358  rpnnen1lem2  10359  rpnnen1lem3  10360  rpnnen1lem4  10361  rpnnen1lem5  10362  xrsupsslem  10641  xrinfmsslem  10642  xrsupss  10643  xrinfmss  10644  iccsupr  10752  flval2  10960  flval3  10961  fsequb  11053  axdc4uzlem  11060  faclbnd4lem4  11325  bccl  11350  hashbc  11407  wrdind  11493  sqrlem3  11746  rexanre  11846  rexico  11853  cau4  11856  caubnd2  11857  caubnd  11858  clim  11984  rlim  11985  rlim2  11986  rlim2lt  11987  rlim3  11988  clim2  11994  clim2c  11995  clim0c  11997  rlim0  11998  rlim0lt  11999  ello12r  12007  ello1d  12013  lo1bdd2  12014  lo1bddrp  12015  elo12r  12018  rlimconst  12034  rlimresb  12055  rlimcld2  12068  climabs0  12075  rlimcn2  12080  reccn2  12086  cn1lem  12087  rlimo1  12106  o1rlimmul  12108  lo1add  12116  lo1mul  12117  isercoll  12157  caucvgrlem  12161  incexclem  12311  climcnds  12326  divrcnv  12327  ruclem12  12535  sqr2irr  12543  gcdcllem1  12706  gcdcllem2  12707  maxprmfct  12808  pc2dvds  12947  pcz  12949  prmpwdvds  12967  infpn2  12976  prmreclem1  12979  prmreclem2  12980  prmreclem3  12981  prmreclem5  12983  prmreclem6  12984  vdwlem6  13049  vdwlem8  13051  vdwlem13  13056  vdwnnlem1  13058  vdwnn  13061  ramz  13088  ramcl  13092  prdsleval  13392  imasval  13430  imasaddfnlem  13446  imasvscafn  13455  mrisval  13548  isacs  13569  isacs2  13571  isacs1i  13575  mreacs  13576  acsfn  13577  acsfn2  13581  catideu  13593  comfeq  13625  catpropd  13628  isnat  13837  isprs  14080  drsdirfi  14088  ispos  14097  lubfval  14128  lubval  14129  lubprop  14130  lubid  14132  glbfval  14133  glbval  14134  glbprop  14135  joinval2  14139  joinlem  14140  meetval2  14146  meetlem  14147  isglbd  14237  lubl  14240  lubun  14243  clatleglb  14246  poslubmo  14266  poslubd  14267  ipodrsima  14284  isdlat  14312  spwval2  14349  spwmo  14351  spwpr2  14353  spwpr4  14356  mgmidmo  14386  ismgmid  14403  ismgmid2  14406  ismndd  14412  mhmima  14456  gsumvallem1  14464  gsumvallem2  14465  gsumvalx  14467  gsumress  14470  gsumval2  14476  gsumwspan  14484  isgrpinv  14548  issubg4  14654  0subg  14658  cycsubgcl  14659  isnsg2  14663  nsgacs  14669  elnmz  14672  ghmrn  14712  ghmnsgima  14722  isga  14761  orbsta  14783  cntzfval  14812  elcntz  14814  resscntz  14823  oppgsubg  14852  odeq  14881  gexid  14908  gexlem2  14909  gexdvds  14911  isslw  14935  pgpssslw  14941  sylow2alem1  14944  sylow2alem2  14945  efgval  15042  efgrelexlemb  15075  efgcpbllemb  15080  gexex  15161  dmdprd  15252  dprd2da  15293  pgpfac1lem5  15330  isabv  15600  islss  15708  lssacs  15740  reslmhm  15825  islbs  15845  pj1lmhm  15869  lbsacsbs  15925  isrrg  16045  opsrval  16232  zlpir  16460  ocvfval  16582  elocv  16584  iunocv  16597  basgen2  16743  bastop1  16747  isclo  16840  ordtbaslem  16934  iscn  16981  cnpval  16982  iscnp  16983  iscnp3  16990  lmbr  17004  lmbr2  17005  lmbrf  17006  cnprest  17033  cnprest2  17034  t0sep  17068  isreg  17076  t1sep2  17113  tgcmp  17144  1stcclb  17186  1stcfb  17187  2ndc1stc  17193  1stcrest  17195  2ndcdisj  17198  islly  17210  isnlly  17211  lly1stc  17238  elkgen  17247  kgencn  17267  elpt  17283  elptr  17284  ptcnplem  17331  tx1stc  17360  cnmpt21  17381  kqt0lem  17443  isr0  17444  regr1lem2  17447  r0sep  17455  nrmr0reg  17456  flffbas  17706  cnflf  17713  cnflf2  17714  lmflf  17716  txflf  17717  fclsopni  17726  fclsnei  17730  fclsrest  17735  fcfnei  17746  cnfcf  17753  alexsubb  17756  alexsubALTlem3  17759  divstgplem  17819  tsmsfbas  17826  tsmsgsum  17837  tsmsres  17842  tsmsf1o  17843  tsmsxplem1  17851  tsmsxp  17853  ismet  17904  isxmet  17905  imasdsf1olem  17953  imasf1oxmet  17955  imasf1omet  17956  metss  18070  met1stc  18083  prdsxmslem2  18091  metcnpi3  18108  txmetcnp  18109  nlmvscn  18214  nrginvrcnlem  18217  nmoval  18240  nmolb  18242  nghmcn  18270  qtopbaslem  18283  icccmplem2  18344  icccmplem3  18345  reconnlem2  18348  metdscn  18376  cncfval  18408  elcncf2  18410  elcncf1di  18415  mulc1cncf  18425  cncfmet  18428  cnllycmp  18470  evth  18473  lebnumlem3  18477  lebnum  18478  xlebnum  18479  ishtpy  18486  isphtpy  18495  pi1xfr  18569  pi1coghm  18575  ipcn  18689  lmmbr2  18701  lmmbr3  18702  lmmbrf  18704  cfilfval  18706  iscfil  18707  fmcfil  18714  caufval  18717  iscau  18718  iscau2  18719  iscau3  18720  iscau4  18721  iscauf  18722  caucfil  18725  cfilresi  18737  causs  18740  lmclim  18744  cncmet  18760  minveclem4c  18805  minveclem2  18806  minveclem3b  18808  minveclem4  18812  minveclem6  18814  minveclem7  18815  ivthlem2  18828  ivthlem3  18829  cniccbdd  18837  ovolunlem1  18872  ovoliunlem1  18877  ovoliun2  18881  ovolicc2lem3  18894  ismbl  18901  ioombl1lem4  18934  uniioombllem2  18954  uniioombllem6  18959  dyadmax  18969  dyadmbllem  18970  dyadmbl  18971  opnmbllem  18972  volcn  18977  ismbf1  18997  ismbf  19001  mbfeqalem  19013  mbfinf  19036  mbflimsup  19037  itg1climres  19085  mbfi1fseqlem6  19091  mbfi1flimlem  19093  itg2seq  19113  itg2monolem1  19121  itg2i1fseq  19126  itg2i1fseq2  19127  itg2cnlem1  19132  itg2cnlem2  19133  isibl  19136  dveflem  19342  ply1divex  19538  fta1g  19569  plyeq0lem  19608  dgrco  19672  plydivex  19693  fta1  19704  vieta1  19708  aannenlem1  19724  aannenlem2  19725  aalioulem2  19729  aalioulem3  19730  ulmval  19775  ulm2  19780  ulmi  19781  ulmres  19783  ulmshftlem  19784  ulmcaulem  19787  ulmcau  19788  ulmss  19790  ulmbdd  19791  ulmdvlem1  19793  ulmdvlem3  19795  iblulm  19799  abelthlem8  19831  pilem2  19844  pilem3  19845  divlogrlim  19998  cxpcn3  20104  dmarea  20268  rlimcnp  20276  cxplim  20282  cxploglim  20288  scvxcvx  20296  emcllem6  20310  ftalem1  20326  ftalem2  20327  ftalem3  20328  isppw2  20369  perfectlem2  20485  2sqlem6  20624  2sqlem10  20629  dchrisumlema  20653  dchrisumlem2  20655  dchrisumlem3  20656  dchrisum0  20685  pntpbnd  20753  pntibndlem3  20757  pntibnd  20758  pntleme  20773  pntlem3  20774  pntlemp  20775  pnt3  20777  isgrpo  20879  isgrpo2  20880  isgrpoi  20881  grpoideu  20892  grpoidinv2  20901  isgrp2d  20918  isgrpda  20980  exidu1  21009  cmpidelt  21012  cnid  21034  mulid  21039  ghgrp  21051  isrngod  21062  rngoideu  21067  cnrngo  21086  vci  21120  isvclem  21149  isnvlem  21182  nvi  21186  nmcvcn  21284  lnoval  21346  islno  21347  isblo3i  21395  blo3i  21396  blocnilem  21398  blocni  21399  ajfval  21403  ubthlem1  21465  ubthlem2  21466  ubthlem3  21467  ubth  21468  minvecolem2  21470  minvecolem3  21471  minvecolem4c  21474  minvecolem4  21475  minvecolem5  21476  minvecolem6  21477  minvecolem7  21478  htthlem  21513  h2hcau  21575  h2hlm  21576  hilid  21756  hcau  21779  hlimi  21783  hlim2  21787  ocel  21876  adjsym  22429  ellnop  22454  ellnfn  22479  hhcno  22500  hhcnf  22501  0cnop  22575  0cnfn  22576  idcnop  22577  lnopeq  22605  elunop2  22609  lnophm  22615  lnconi  22629  lnopcnbd  22632  lnfncnbd  22653  imaelshi  22654  riesz3i  22658  riesz4i  22659  riesz4  22660  riesz1  22661  cnlnadjlem2  22664  cnlnadjlem5  22667  cnlnadjlem8  22670  cnlnadji  22672  nmopadjlei  22684  cnvbraval  22706  leopg  22718  leoppos  22722  mdbr  22890  dmdbr  22895  cdj3i  23037  ballotleme  23071  funcnv5mpt  23251  rge0scvg  23388  esumpcvgval  23461  isrnmeas  23546  ismbfm  23572  isanmbfm  23576  mbfmcst  23579  derangenlem  23717  subfacp1lem3  23728  subfacp1lem5  23730  subfacp1lem6  23731  subfacp1  23732  erdszelem8  23744  kur14  23762  cnpcon  23776  rescon  23792  cvmscbv  23804  iscvm  23805  cvmsi  23811  cvmsval  23812  cvmlift3lem2  23866  iseupa  23896  snmlval  23929  ghomgrpilem1  24007  dedekind  24097  dedekindle  24098  faclimlem5  24121  dfpo2  24183  dfon2lem9  24218  dfrdg2  24223  dfrdg3  24224  poseq  24324  soseq  24325  wfrlem1  24327  wfrlem15  24341  frrlem1  24352  sltval  24372  nocvxminlem  24415  nobndlem2  24418  nobndlem8  24424  nobndup  24425  nobnddown  24426  brbtwn2  24605  colinearalg  24610  axsegconlem1  24617  axsegcon  24627  ax5seglem4  24632  ax5seglem5  24633  axlowdim  24661  axeuclidlem  24662  axcontlem1  24664  axcontlem2  24665  axcontlem4  24667  axcontlem5  24668  axcontlem8  24671  axcontlem12  24675  bpolylem  24855  bpolyval  24856  supaddc  24995  supadd  24996  itg2addnc  25005  elixp2b  25257  prjmapcp2  25273  islatalg  25286  ubos  25359  puub2  25361  puub  25362  supdef  25365  ismxl2  25370  ismnl2  25371  defge3  25374  defse3  25375  clfsebsr  25452  idlvalNEW  25548  isidlNEW  25549  vecval1b  25554  vecval3b  25555  vri  25595  basexre  25625  usptoplem  25649  istopx  25650  usptop  25653  prcnt  25654  cnfilca  25659  flfnei2  25680  tcnvec  25793  isded  25839  dedi  25840  iscatOLD  25857  cati  25858  isfunb  25938  isntr  25976  islimcat  25979  indcls2  26099  pfsubkl  26150  isibg2  26213  isibg2aa  26215  isibg2aalem1  26216  isibg2aalem2  26217  bsstrs  26249  nbssntrs  26250  isibcg  26294  nn0prpwlem  26341  isfne  26371  isfne4  26372  isfne2  26374  isfne3  26375  isref  26382  islocfin  26399  neibastop3  26414  topmeet  26416  topjoin  26417  filnetlem4  26433  f1opr  26494  upixp  26506  indexdom  26516  filbcmb  26535  sdclem2  26555  fdc  26558  lmclim2  26577  caures  26579  istotbnd  26596  istotbnd3  26598  sstotbnd  26602  isbnd  26607  heibor  26648  bfp  26651  rrncmslem  26659  exidres  26671  exidresid  26672  idlval  26741  isidl  26742  0idl  26753  unichnidl  26759  pridl  26765  ismaxidl  26768  smprngopr  26780  igenval2  26794  prnc  26795  ispridlc  26798  isnacs  26882  isnacs2  26884  nacsfix  26890  mzpclval  26906  elmzpcl  26907  rencldnfilem  27006  infmrgelbi  27066  pellfundre  27069  pellfundlb  27072  wepwsolem  27241  fnwe2lem2  27251  aomclem8  27262  dfac11  27263  frlmlbs  27352  gicabl  27366  islindf  27385  islinds2  27386  islindf2  27387  lindfrn  27394  lsslindf  27403  islindf4  27411  islnr3  27422  hbtlem2  27431  hbtlem5  27435  psgnunilem2  27521  psgnunilem3  27522  ubelsupr  27794  evthf  27801  fnchoice  27803  stoweidlem5  27857  stoweidlem9  27861  stoweidlem15  27867  stoweidlem16  27868  stoweidlem27  27879  stoweidlem28  27880  stoweidlem31  27883  stoweidlem34  27886  stoweidlem37  27889  stoweidlem46  27898  stoweidlem48  27900  stoweidlem51  27903  stoweidlem52  27904  stoweidlem59  27911  wallispilem3  27919  stirlinglem13  27938  cbvral2  28053  raaan2  28056  2reu4a  28070  dfdfat2  28099  hashgt12el  28218  cusgra3v  28299  wlks  28328  wlkntrllem5  28349  constr3trllem2  28397  bnj1185  29142  bnj1385  29181  bnj66  29208  bnj106  29216  bnj155  29227  bnj852  29269  bnj893  29276  bnj1228  29357  bnj1234  29359  bnj1463  29401  lubunNEW  29785  islfl  29872  eqlkr  29911  eqlkr3  29913  glbconN  30188  hlsuprexch  30192  ispsubsp  30556  ldilset  30920  isldil  30921  dilsetN  30964  isdilN  30965  trlset  30972  trlval  30973  cdleme27b  31179  cdleme29b  31186  cdleme31so  31190  cdleme31sn1  31192  cdleme31sn1c  31199  cdleme31fv  31201  cdleme40v  31280  istendo  31571  cdlemkid3N  31744  cdlemkid4  31745  cdlemkid5  31746  dihfval  32043  dihval  32044  islpolN  32295  hdmapffval  32641  hdmapfval  32642  hdmapval  32643  hdmapval2lem  32646  hgmapffval  32700  hgmapfval  32701  hgmapval  32702  hgmapvs  32706
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1535  df-ral 2561
  Copyright terms: Public domain W3C validator