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

Theorem ralbidv 2717
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 1629 . 2  |-  F/ x ph
2 ralbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2ralbid 2715 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wral 2697
This theorem is referenced by:  ralbii  2721  2ralbidv  2739  rexralbidv  2741  raleqbi1dv  2904  raleqbidv  2908  cbvral2v  2932  rspc2  3049  rspc3v  3053  reu6i  3117  reu7  3121  sbcralt  3225  sbcralg  3227  raaan  3727  raaanv  3728  r19.12sn  3864  2ralunsn  3996  elintg  4050  elintrabg  4055  eliin  4090  disjprg  4200  disjxun  4202  poeq1  4498  somo  4529  frirr  4551  fr2nr  4552  frminex  4554  wereu2  4571  reusv2lem2  4717  reusv3  4723  reusv6OLD  4726  fr3nr  4752  onssmin  4769  posn  4938  frsn  4940  ralxpf  5011  cnvpo  5402  funcnvuni  5510  iinpreima  5852  dff4  5875  dff13f  5998  f1oweALT  6066  ofreq  6300  frxp  6448  sorpssuni  6523  sorpssint  6524  eusvobj2  6574  riotasvd  6584  smoeq  6604  recseq  6626  tfrlem3  6630  tfrlem3a  6631  tfrlem12  6642  tz7.48lem  6690  elixp2  7058  undifixp  7090  xpf1o  7261  nneneq  7282  ac6sfi  7343  frfi  7344  fipreima  7404  indexfi  7406  marypha1lem  7430  marypha1  7431  supeq1  7442  supeq3  7446  supmo  7449  eqsup  7453  supub  7456  suplub  7457  supmaxlem  7461  supisoex  7468  oieq1  7473  ordtypecbv  7478  ordtypelem3  7481  ordtypelem6  7484  ordtypelem7  7485  ordtypelem9  7487  wemaplem1  7507  wemaplem2  7508  zfregcl  7554  oemapval  7631  oemapvali  7632  cantnf  7641  wemapwe  7646  rankval3b  7744  unbndrank  7760  rankunb  7768  rankuni2b  7771  tcrank  7800  scottex  7801  scottexs  7803  scott0s  7804  bnd2  7809  dfac8clem  7905  ac5num  7909  acni  7918  acni2  7919  alephval3  7983  dfac4  7995  dfac5lem5  8000  dfac5  8001  dfac2a  8002  dfac2  8003  dfacacn  8013  kmlem2  8023  kmlem13  8034  cflem  8118  cflecard  8125  cfeq0  8128  cfsuc  8129  cfflb  8131  cofsmo  8141  cfsmolem  8142  cfcoflem  8144  coftr  8145  alephsing  8148  fin23lem11  8189  isfin3ds  8201  fin23lem17  8210  fin23lem39  8222  isf33lem  8238  isf34lem6  8252  fin1a2lem13  8284  hsmexlem4  8301  hsmex  8304  axcc2lem  8308  axcc3  8310  dcomex  8319  axdc2lem  8320  axdc3lem2  8323  axdc3lem3  8324  axdc3  8326  axdc4lem  8327  axcclem  8329  zorn2lem2  8369  zorn2lem7  8374  zorn2g  8375  zornn0g  8377  ttukeylem7  8387  axdclem2  8392  brdom3  8398  brdom7disj  8401  brdom6disj  8402  alephval2  8439  inar1  8642  axgroth6  8695  pinq  8796  nqereu  8798  prlem934  8902  supexpr  8923  supsrlem  8978  axpre-sup  9036  fimaxre2  9948  lbreu  9950  sup2  9956  infm3  9959  supmul1  9965  supmullem2  9967  supmul  9968  infmrcl  9979  nnsub  10030  uzwo  10531  uzwoOLD  10532  nnwof  10535  uzinfmi  10547  ublbneg  10552  lbzbi  10556  zsupss  10557  uzsupss  10560  uzwo3  10561  zmax  10563  rpnnen1lem1  10592  rpnnen1lem2  10593  rpnnen1lem3  10594  rpnnen1lem4  10595  rpnnen1lem5  10596  xrsupsslem  10877  xrinfmsslem  10878  xrsupss  10879  xrinfmss  10880  iccsupr  10989  flval2  11213  flval3  11214  fsequb  11306  axdc4uzlem  11313  faclbnd4lem4  11579  bccl  11605  hashgt12el  11674  hashbc  11694  wrdind  11783  sqrlem3  12042  rexanre  12142  rexico  12149  cau4  12152  caubnd2  12153  caubnd  12154  clim  12280  rlim  12281  rlim2  12282  rlim2lt  12283  rlim3  12284  clim2  12290  clim2c  12291  clim0c  12293  rlim0  12294  rlim0lt  12295  ello12r  12303  ello1d  12309  lo1bdd2  12310  lo1bddrp  12311  elo12r  12314  rlimconst  12330  rlimresb  12351  rlimcld2  12364  climabs0  12371  rlimcn2  12376  reccn2  12382  cn1lem  12383  rlimo1  12402  o1rlimmul  12404  lo1add  12412  lo1mul  12413  isercoll  12453  caucvgrlem  12458  incexclem  12608  climcnds  12623  divrcnv  12624  ruclem12  12832  sqr2irr  12840  gcdcllem1  13003  gcdcllem2  13004  maxprmfct  13105  pc2dvds  13244  pcz  13246  prmpwdvds  13264  infpn2  13273  prmreclem1  13276  prmreclem2  13277  prmreclem3  13278  prmreclem5  13280  prmreclem6  13281  vdwlem6  13346  vdwlem8  13348  vdwlem13  13353  vdwnnlem1  13355  vdwnn  13358  ramz  13385  ramcl  13389  prdsleval  13691  imasval  13729  imasaddfnlem  13745  imasvscafn  13754  mrisval  13847  isacs  13868  isacs2  13870  isacs1i  13874  mreacs  13875  acsfn  13876  acsfn2  13880  iscatd  13890  catidex  13891  catideu  13892  cidval  13894  catidd  13897  comfeq  13924  catpropd  13927  ismon  13951  isfunc  14053  isnat  14136  isprs  14379  drsdirfi  14387  ispos  14396  lubfval  14427  lubval  14428  lubprop  14429  lubid  14431  glbfval  14432  glbval  14433  glbprop  14434  joinval2  14438  joinlem  14439  meetval2  14445  meetlem  14446  isglbd  14536  lubl  14539  lubun  14542  clatleglb  14545  poslubmo  14565  poslubd  14566  ipodrsima  14583  isdlat  14611  spwval2  14648  spwmo  14650  spwpr2  14652  spwpr4  14655  mgmidmo  14685  ismgmid  14702  ismgmid2  14705  ismndd  14711  mhmima  14755  gsumvallem1  14763  gsumvallem2  14764  gsumvalx  14766  gsumress  14769  gsumval2  14775  gsumwspan  14783  isgrpinv  14847  issubg4  14953  0subg  14957  cycsubgcl  14958  isnsg2  14962  nsgacs  14968  elnmz  14971  ghmrn  15011  ghmnsgima  15021  isga  15060  orbsta  15082  cntzfval  15111  elcntz  15113  resscntz  15122  oppgsubg  15151  odeq  15180  gexid  15207  gexlem2  15208  gexdvds  15210  isslw  15234  pgpssslw  15240  sylow2alem1  15243  sylow2alem2  15244  efgval  15341  efgrelexlemb  15374  efgcpbllemb  15379  gexex  15460  dmdprd  15551  dprd2da  15592  pgpfac1lem5  15629  isabv  15899  islss  16003  lssacs  16035  reslmhm  16120  islbs  16140  pj1lmhm  16164  lbsacsbs  16220  isrrg  16340  opsrval  16527  zlpir  16763  ocvfval  16885  elocv  16887  iunocv  16900  basgen2  17046  bastop1  17050  isclo  17143  ordtbaslem  17244  iscn  17291  cnpval  17292  iscnp  17293  iscnp3  17300  lmbr  17314  lmbr2  17315  lmbrf  17316  cnprest  17345  cnprest2  17346  t0sep  17380  isreg  17388  t1sep2  17425  tgcmp  17456  1stcclb  17499  1stcfb  17500  2ndc1stc  17506  1stcrest  17508  2ndcdisj  17511  islly  17523  isnlly  17524  lly1stc  17551  elkgen  17560  kgencn  17580  elpt  17596  elptr  17597  ptcnplem  17645  tx1stc  17674  cnmpt21  17695  kqt0lem  17760  isr0  17761  regr1lem2  17764  r0sep  17772  nrmr0reg  17773  flffbas  18019  cnflf  18026  cnflf2  18027  lmflf  18029  txflf  18030  fclsopni  18039  fclsnei  18043  fclsrest  18048  fcfnei  18059  cnfcf  18066  alexsubb  18069  alexsubALTlem3  18072  divstgplem  18142  tsmsfbas  18149  tsmsgsum  18160  tsmsres  18165  tsmsf1o  18166  tsmsxplem1  18174  tsmsxp  18176  ustval  18224  isust  18225  ustincl  18229  ustdiag  18230  ustinvel  18231  ustexhalf  18232  ust0  18241  utopval  18254  ucnval  18299  isucn  18300  isucn2  18301  ucnima  18303  iscfilu  18310  ispsmet  18327  ismet  18345  isxmet  18346  imasdsf1olem  18395  imasf1oxmet  18397  imasf1omet  18398  metss  18530  met1stc  18543  prdsxmslem2  18551  metcnpi3  18568  txmetcnp  18569  metucnOLD  18610  metucn  18611  nlmvscn  18715  nrginvrcnlem  18718  nmoval  18741  nmolb  18743  nghmcn  18771  qtopbaslem  18784  icccmplem2  18846  icccmplem3  18847  reconnlem2  18850  metdscn  18878  cncfval  18910  elcncf2  18912  elcncf1di  18917  mulc1cncf  18927  cncfmet  18930  cnllycmp  18973  evth  18976  lebnumlem3  18980  lebnum  18981  xlebnum  18982  ishtpy  18989  isphtpy  18998  pi1xfr  19072  pi1coghm  19078  ipcn  19192  lmmbr2  19204  lmmbr3  19205  lmmbrf  19207  cfilfval  19209  iscfil  19210  fmcfil  19217  caufval  19220  iscau  19221  iscau2  19222  iscau3  19223  iscau4  19224  iscauf  19225  caucfil  19228  cfilresi  19240  causs  19243  lmclim  19247  cncmet  19267  cmetcusp1OLD  19297  cmetcusp1  19298  minveclem4c  19318  minveclem2  19319  minveclem3b  19321  minveclem4  19325  minveclem6  19327  minveclem7  19328  ivthlem2  19341  ivthlem3  19342  cniccbdd  19350  ovolunlem1  19385  ovoliunlem1  19390  ovoliun2  19394  ovolicc2lem3  19407  ismbl  19414  ioombl1lem4  19447  uniioombllem2  19467  uniioombllem6  19472  dyadmax  19482  dyadmbllem  19483  dyadmbl  19484  opnmbllem  19485  volcn  19490  ismbf1  19510  ismbf  19514  mbfeqalem  19526  mbfinf  19549  mbflimsup  19550  itg1climres  19598  mbfi1fseqlem6  19604  mbfi1flimlem  19606  itg2seq  19626  itg2monolem1  19634  itg2i1fseq  19639  itg2i1fseq2  19640  itg2cnlem1  19645  itg2cnlem2  19646  isibl  19649  dveflem  19855  ply1divex  20051  fta1g  20082  plyeq0lem  20121  dgrco  20185  plydivex  20206  fta1  20217  vieta1  20221  aannenlem1  20237  aannenlem2  20238  aalioulem2  20242  aalioulem3  20243  ulmval  20288  ulm2  20293  ulmi  20294  ulmres  20296  ulmshftlem  20297  ulmcaulem  20302  ulmcau  20303  ulmss  20305  ulmbdd  20306  ulmdvlem1  20308  ulmdvlem3  20310  mtestbdd  20313  iblulm  20315  abelthlem8  20347  pilem2  20360  pilem3  20361  divlogrlim  20518  cxpcn3  20624  dmarea  20788  rlimcnp  20796  cxplim  20802  cxploglim  20808  scvxcvx  20816  emcllem6  20831  ftalem1  20847  ftalem2  20848  ftalem3  20849  isppw2  20890  perfectlem2  21006  2sqlem6  21145  2sqlem10  21150  dchrisumlema  21174  dchrisumlem2  21176  dchrisumlem3  21177  dchrisum0  21206  pntpbnd  21274  pntibndlem3  21278  pntibnd  21279  pntleme  21294  pntlem3  21295  pntlemp  21296  pnt3  21298  cusgra3v  21465  wlks  21518  wlkntrllem3  21553  constr3trllem2  21630  1conngra  21654  iseupa  21679  isgrpo  21776  isgrpo2  21777  isgrpoi  21778  grpoideu  21789  grpoidinv2  21798  isgrp2d  21815  isgrpda  21877  exidu1  21906  cmpidelt  21909  cnid  21931  mulid  21936  ghgrp  21948  isrngod  21959  rngoideu  21964  cnrngo  21983  vci  22019  isvclem  22048  isnvlem  22081  nvi  22085  nmcvcn  22183  lnoval  22245  islno  22246  isblo3i  22294  blo3i  22295  blocnilem  22297  blocni  22298  ajfval  22302  ubthlem1  22364  ubthlem2  22365  ubthlem3  22366  ubth  22367  minvecolem2  22369  minvecolem3  22370  minvecolem4c  22373  minvecolem4  22374  minvecolem5  22375  minvecolem6  22376  minvecolem7  22377  htthlem  22412  h2hcau  22474  h2hlm  22475  hilid  22655  hcau  22678  hlimi  22682  hlim2  22686  ocel  22775  adjsym  23328  ellnop  23353  ellnfn  23378  hhcno  23399  hhcnf  23400  0cnop  23474  0cnfn  23475  idcnop  23476  lnopeq  23504  elunop2  23508  lnophm  23514  lnconi  23528  lnopcnbd  23531  lnfncnbd  23552  imaelshi  23553  riesz3i  23557  riesz4i  23558  riesz4  23559  riesz1  23560  cnlnadjlem2  23563  cnlnadjlem5  23566  cnlnadjlem8  23569  cnlnadji  23571  nmopadjlei  23583  cnvbraval  23605  leopg  23617  leoppos  23621  mdbr  23789  dmdbr  23794  cdj3i  23936  funcnv5mpt  24076  resspos  24179  isofld  24227  ofldadd  24230  ofldmul  24231  inftmrel  24242  isinftm  24243  rge0scvg  24327  qqhcn  24367  esumpcvgval  24460  sigaval  24485  issgon  24498  isrnmeas  24546  ismbfm  24594  isanmbfm  24598  mbfmcst  24601  sitgval  24639  ballotleme  24746  lgamgulmlem2  24806  lgamgulmlem3  24807  lgamgulmlem5  24809  lgambdd  24813  lgamcvglem  24816  derangenlem  24849  subfacp1lem3  24860  subfacp1lem5  24862  subfacp1lem6  24863  subfacp1  24864  erdszelem8  24876  kur14  24894  cnpcon  24909  rescon  24925  cvmscbv  24937  iscvm  24938  cvmsi  24944  cvmsval  24945  cvmlift3lem2  24999  snmlval  25010  ghomgrpilem1  25088  dedekind  25179  dedekindle  25180  dfpo2  25370  dfon2lem9  25410  dfrdg2  25415  dfrdg3  25416  poseq  25520  soseq  25521  wrecseq123  25524  wfrlem1  25530  wfrlem15  25544  frrlem1  25574  sltval  25594  nocvxminlem  25637  nobndlem2  25640  nobndlem8  25646  nobndup  25647  nobnddown  25648  brbtwn2  25836  colinearalg  25841  axsegconlem1  25848  axsegcon  25858  ax5seglem4  25863  ax5seglem5  25864  axlowdim  25892  axeuclidlem  25893  axcontlem1  25895  axcontlem2  25896  axcontlem4  25898  axcontlem5  25899  axcontlem8  25902  axcontlem12  25906  supaddc  26228  supadd  26229  mblfinlem  26234  mblfinlem2  26235  ismblfin  26237  voliunnfl  26240  volsupnfl  26241  mbfresfi  26243  itg2addnc  26249  ftc1anc  26278  nn0prpwlem  26316  isfne  26339  isfne4  26340  isfne2  26342  isfne3  26343  isref  26350  islocfin  26367  neibastop3  26382  topmeet  26384  topjoin  26385  filnetlem4  26401  f1opr  26417  upixp  26422  indexdom  26427  filbcmb  26433  sdclem2  26437  fdc  26440  lmclim2  26455  caures  26457  istotbnd  26469  istotbnd3  26471  sstotbnd  26475  isbnd  26480  heibor  26521  bfp  26524  rrncmslem  26532  exidres  26544  exidresid  26545  idlval  26614  isidl  26615  0idl  26626  unichnidl  26632  pridl  26638  ismaxidl  26641  smprngopr  26653  igenval2  26667  prnc  26668  ispridlc  26671  isnacs  26749  isnacs2  26751  nacsfix  26757  mzpclval  26773  elmzpcl  26774  rencldnfilem  26872  infmrgelbi  26932  pellfundre  26935  pellfundlb  26938  wepwsolem  27107  fnwe2lem2  27117  aomclem8  27127  dfac11  27128  frlmlbs  27217  gicabl  27231  islindf  27250  islinds2  27251  islindf2  27252  lindfrn  27259  lsslindf  27268  islindf4  27276  islnr3  27287  hbtlem2  27296  hbtlem5  27300  psgnunilem2  27386  psgnunilem3  27387  evth2f  27653  ubelsupr  27658  evthf  27665  fnchoice  27667  stoweidlem5  27721  stoweidlem9  27725  stoweidlem15  27731  stoweidlem16  27732  stoweidlem27  27743  stoweidlem28  27744  stoweidlem31  27747  stoweidlem34  27750  stoweidlem37  27753  stoweidlem46  27762  stoweidlem48  27764  stoweidlem51  27767  stoweidlem52  27768  stoweidlem59  27775  wallispilem3  27783  stirlinglem13  27802  cbvral2  27917  raaan2  27920  2reu4a  27934  dfdfat2  27962  reumodprminv  28193  cshw1v  28239  cshwssizesame  28251  frgrawopreg1  28376  frgrawopreg2  28377  bnj1185  29102  bnj1385  29141  bnj66  29168  bnj106  29176  bnj155  29187  bnj852  29229  bnj893  29236  bnj1228  29317  bnj1234  29319  bnj1463  29361  lubunNEW  29708  islfl  29795  eqlkr  29834  eqlkr3  29836  glbconN  30111  hlsuprexch  30115  ispsubsp  30479  ldilset  30843  isldil  30844  dilsetN  30887  isdilN  30888  trlset  30895  trlval  30896  cdleme27b  31102  cdleme29b  31109  cdleme31so  31113  cdleme31sn1  31115  cdleme31sn1c  31122  cdleme31fv  31124  cdleme40v  31203  istendo  31494  cdlemkid3N  31667  cdlemkid4  31668  cdlemkid5  31669  dihfval  31966  dihval  31967  islpolN  32218  hdmapffval  32564  hdmapfval  32565  hdmapval  32566  hdmapval2lem  32569  hgmapffval  32623  hgmapfval  32624  hgmapval  32625  hgmapvs  32629
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-ral 2702
  Copyright terms: Public domain W3C validator