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

Theorem ralbidva 2561
Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 4-Mar-1997.)
Hypothesis
Ref Expression
ralbidva.1  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
Assertion
Ref Expression
ralbidva  |-  ( 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 ralbidva
StepHypRef Expression
1 nfv 1607 . 2  |-  F/ x ph
2 ralbidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2ralbida 2559 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    e. wcel 1686   A.wral 2545
This theorem is referenced by:  raleqbidva  2752  ordunisssuc  4497  tfindsg2  4654  poinxp  4755  soinxp  4756  frinxp  4757  funimass3  5643  fnsuppres  5734  cocan1  5803  cocan2  5804  isores2  5832  isoini2  5838  f1oweALT  5853  ofrfval  6088  ofrfval2  6098  dfsmo2  6366  smores  6371  smores2  6373  ac6sfi  7103  fimaxg  7106  ordunifi  7109  isfinite2  7117  fipreima  7163  supisolem  7223  ordiso2  7232  ordtypelem7  7241  cantnf  7397  wemapwe  7402  rankval3b  7500  rankonidlem  7502  iscard  7610  acndom  7680  dfac12lem3  7773  kmlem2  7779  cflim2  7891  cfsmolem  7898  ttukeylem6  8143  alephreg  8206  suplem2pr  8679  axsup  8900  sup3  9713  infm3  9715  suprleub  9720  dfinfmr  9733  infmrgelb  9736  ofsubeq0  9745  ofsubge0  9747  zextlt  10088  prime  10094  indstr  10289  supxr2  10634  supxrbnd1  10642  supxrbnd2  10643  supxrleub  10647  supxrbnd  10649  infmxrgelb  10655  fzshftral  10871  clim  11970  rlim  11971  clim2  11980  clim2c  11981  clim0c  11983  ello1mpt  11997  lo1o1  12008  o1lo1  12013  climabs0  12061  o1compt  12063  rlimdiv  12121  geomulcvg  12334  mertenslem2  12343  mertens  12344  rpnnen2  12506  sqr2irr  12529  pc11  12934  pcz  12935  1arith  12976  vdwlem8  13037  vdwlem11  13040  vdw  13043  ramval  13057  pwsle  13393  mrieqvd  13542  mreacs  13562  cidpropd  13615  ismon2  13639  monpropd  13642  isepi  13645  isepi2  13646  subsubc  13729  funcres2b  13773  funcpropd  13776  isfull2  13787  isfth2  13791  fucsect  13848  fucinv  13849  pospropd  14240  ipodrsfi  14268  tsrss  14334  mndpropd  14400  grpidpropd  14401  grppropd  14502  issubg4  14640  gass  14757  gexdvds  14897  gexdvds2  14898  subgpgp  14910  sylow3lem6  14945  efgval2  15035  efgsp1  15048  dprdf11  15260  subgdmdprd  15271  rngpropd  15374  abvpropd  15609  lsspropd  15776  lbspropd  15854  assapropd  16069  psrbaglefi  16120  psrbagconf1o  16122  gsumbagdiaglem  16123  mplmonmul  16210  phlpropd  16561  ishil2  16621  tgss2  16727  isclo  16826  neips  16852  opnnei  16859  isperf3  16886  ssidcn  16987  lmbrf  16992  cnrest2  17016  lmss  17028  lmres  17030  ist1-2  17077  ist1-3  17079  isreg2  17107  cmpfi  17137  1stccn  17191  subislly  17209  kgencn  17253  ptclsg  17311  ptcnplem  17317  xkococnlem  17355  xkoinjcn  17383  tgqtop  17405  qtopcn  17407  fbflim  17673  flimrest  17680  flfnei  17688  isflf  17690  cnflf  17699  fclsopn  17711  fclsbas  17718  fclsrest  17721  isfcf  17731  cnfcf  17739  ptcmplem3  17750  tmdgsum2  17781  eltsms  17817  tsmsgsum  17823  tsmssubm  17827  tsmsf1o  17829  ismet2  17900  prdsxmetlem  17934  elmopn2  17993  prdsbl  18039  metss  18056  metrest  18072  metcnp  18089  metcnp2  18090  metcn  18091  nrginvrcn  18204  metdsge  18355  divcn  18374  elcncf2  18396  mulc1cncf  18411  cncfmet  18414  evth2  18460  lmmbr2  18687  lmmbrf  18690  iscfil2  18694  cfil3i  18697  iscau2  18705  iscau4  18707  iscauf  18708  caucfil  18711  iscmet3lem3  18718  cfilres  18724  causs  18726  lmclim  18730  evthicc2  18822  cniccbdd  18823  ovolfioo  18829  ovolficc  18830  ismbl2  18888  mbfsup  19021  mbfinf  19022  mbflimsup  19023  0plef  19029  mbfi1flim  19080  xrge0f  19088  itg2mulclem  19103  itgeqa  19170  ellimc2  19229  ellimc3  19231  limcflf  19233  cnlimc  19240  dvferm1  19334  dvferm2  19336  rolle  19339  dvivthlem1  19357  ftc1lem6  19390  itgsubst  19398  mdegle0  19465  deg1leb  19483  plydivex  19679  ulm2  19766  ulmcaulem  19773  ulmcau  19774  ulmdvlem3  19781  abelthlem9  19818  abelth  19819  rlimcnp  20262  ftalem3  20314  issqf  20376  sqf11  20379  dvdsmulf1o  20436  dchrelbas4  20484  dchrinv  20502  2sqlem6  20610  chpo1ubb  20632  dchrmusumlema  20644  dchrisum0lema  20665  ostth3  20789  isgrpo2  20866  nmounbi  21356  blocnilem  21384  isph  21402  phoeqi  21438  h2hcau  21561  h2hlm  21562  hial2eq2  21688  hoeq1  22412  hoeq2  22413  adjsym  22415  cnvadj  22474  hhcno  22486  hhcnf  22487  adjvalval  22519  leop2  22706  leoptri  22718  mdbr2  22878  dmdbr2  22885  mddmd2  22891  cdj3lem3b  23022  lmdvg  23378  subfacp1lem3  23715  subfacp1lem5  23717  dfrdg2  24154  tfrALTlem  24278  eqeelen  24534  brbtwn2  24535  colinearalg  24540  axcgrid  24546  axsegconlem1  24547  ax5seglem4  24562  ax5seglem5  24563  axbtwnid  24569  axpasch  24571  axeuclidlem  24592  axcontlem2  24595  axcontlem4  24597  axcontlem7  24600  axcontlem12  24605  surjsec2  25131  prl2  25180  idlvalNEW  25456  istopxc  25559  lvsovso2  25638  supnuf  25640  supexr  25642  tcnvec  25701  opnrebl  26246  lmclim2  26485  caures  26487  sstotbnd2  26509  rrnmet  26564  rrncmslem  26567  isdrngo3  26601  isidlc  26651  fnnfpeq0  26769  wepwsolem  27149  fnwe2lem2  27159  islnm2  27187  lindfmm  27308  islindf4  27319  islindf5  27320  caofcan  27551  cvrval2  29537  isat3  29570  iscvlat2N  29587  glbconN  29639  ltrneq  30411  cdlemefrs29clN  30661  cdlemefrs32fva  30662  cdleme32fva  30699  cdlemk33N  31171  cdlemk34  31172  cdlemkid3N  31195  cdlemkid4  31196  diaglbN  31318  dibglbN  31429  dihglbcpreN  31563  dihglblem6  31603  hdmap1eulem  32087  hdmap1eulemOLDN  32088  hdmapoc  32197  hlhilocv  32223
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-11 1717
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1534  df-ral 2550
  Copyright terms: Public domain W3C validator