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

Theorem ralbidva 2723
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 1630 . 2  |-  F/ x ph
2 ralbidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2ralbida 2721 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    e. wcel 1726   A.wral 2707
This theorem is referenced by:  raleqbidva  2920  ordunisssuc  4686  tfindsg2  4843  poinxp  4943  soinxp  4944  frinxp  4945  funimass3  5848  fnsuppres  5954  cocan1  6026  cocan2  6027  isores2  6055  isoini2  6061  f1oweALT  6076  ofrfval  6315  ofrfval2  6325  dfsmo2  6611  smores  6616  smores2  6618  ac6sfi  7353  fimaxg  7356  ordunifi  7359  isfinite2  7367  fipreima  7414  supisolem  7477  ordiso2  7486  ordtypelem7  7495  cantnf  7651  wemapwe  7656  rankval3b  7754  rankonidlem  7756  iscard  7864  acndom  7934  dfac12lem3  8027  kmlem2  8033  cflim2  8145  cfsmolem  8152  ttukeylem6  8396  alephreg  8459  suplem2pr  8932  axsup  9153  sup3  9967  infm3  9969  suprleub  9974  dfinfmr  9987  infmrgelb  9990  ofsubeq0  9999  ofsubge0  10001  zextlt  10346  prime  10352  indstr  10547  supxr2  10894  supxrbnd1  10902  supxrbnd2  10903  supxrleub  10907  supxrbnd  10909  infmxrgelb  10915  fzshftral  11136  clim  12290  rlim  12291  clim2  12300  clim2c  12301  clim0c  12303  ello1mpt  12317  lo1o1  12328  o1lo1  12333  climabs0  12381  o1compt  12383  rlimdiv  12441  geomulcvg  12655  mertenslem2  12664  mertens  12665  rpnnen2  12827  sqr2irr  12850  pc11  13255  pcz  13256  1arith  13297  vdwlem8  13358  vdwlem11  13361  vdw  13364  ramval  13378  pwsle  13716  mrieqvd  13865  mreacs  13885  cidpropd  13938  ismon2  13962  monpropd  13965  isepi  13968  isepi2  13969  subsubc  14052  funcres2b  14096  funcpropd  14099  isfull2  14110  isfth2  14114  fucsect  14171  fucinv  14172  pospropd  14563  ipodrsfi  14591  tsrss  14657  mndpropd  14723  grpidpropd  14724  grppropd  14825  issubg4  14963  gass  15080  gexdvds  15220  gexdvds2  15221  subgpgp  15233  sylow3lem6  15268  efgval2  15358  efgsp1  15371  dprdf11  15583  subgdmdprd  15594  rngpropd  15697  abvpropd  15932  lsspropd  16095  lbspropd  16173  assapropd  16388  psrbaglefi  16439  psrbagconf1o  16441  gsumbagdiaglem  16442  mplmonmul  16529  phlpropd  16888  ishil2  16948  tgss2  17054  isclo  17153  neips  17179  opnnei  17186  isperf3  17219  ssidcn  17321  lmbrf  17326  cnnei  17348  cnrest2  17352  lmss  17364  lmres  17366  ist1-2  17413  ist1-3  17415  isreg2  17443  cmpfi  17473  1stccn  17528  subislly  17546  kgencn  17590  ptclsg  17649  ptcnplem  17655  xkococnlem  17693  xkoinjcn  17721  tgqtop  17746  qtopcn  17748  fbflim  18010  flimrest  18017  flfnei  18025  isflf  18027  cnflf  18036  fclsopn  18048  fclsbas  18055  fclsrest  18058  isfcf  18068  cnfcf  18076  ptcmplem3  18087  tmdgsum2  18128  eltsms  18164  tsmsgsum  18170  tsmssubm  18174  tsmsf1o  18176  utopsnneiplem  18279  ismet2  18365  prdsxmetlem  18400  elmopn2  18477  prdsbl  18523  metss  18540  metrest  18556  metcnp  18573  metcnp2  18574  metcn  18575  metucnOLD  18620  metucn  18621  nrginvrcn  18729  metdsge  18881  divcn  18900  elcncf2  18922  mulc1cncf  18937  cncfmet  18940  evth2  18987  lmmbr2  19214  lmmbrf  19217  iscfil2  19221  cfil3i  19224  iscau2  19232  iscau4  19234  iscauf  19235  caucfil  19238  iscmet3lem3  19245  cfilres  19251  causs  19253  lmclim  19257  evthicc2  19359  cniccbdd  19360  ovolfioo  19366  ovolficc  19367  ismbl2  19425  mbfsup  19558  mbfinf  19559  mbflimsup  19560  0plef  19566  mbfi1flim  19617  xrge0f  19625  itg2mulclem  19640  itgeqa  19707  ellimc2  19766  ellimc3  19768  limcflf  19770  cnlimc  19777  dvferm1  19871  dvferm2  19873  rolle  19876  dvivthlem1  19894  ftc1lem6  19927  itgsubst  19935  mdegle0  20002  deg1leb  20020  plydivex  20216  ulm2  20303  ulmcaulem  20312  ulmcau  20313  ulmdvlem3  20320  abelthlem9  20358  abelth  20359  rlimcnp  20806  ftalem3  20859  issqf  20921  sqf11  20924  dvdsmulf1o  20981  dchrelbas4  21029  dchrinv  21047  2sqlem6  21155  chpo1ubb  21177  dchrmusumlema  21189  dchrisum0lema  21210  ostth3  21334  isgrpo2  21787  nmounbi  22279  blocnilem  22307  isph  22325  phoeqi  22361  h2hcau  22484  h2hlm  22485  hial2eq2  22611  hoeq1  23335  hoeq2  23336  adjsym  23338  cnvadj  23397  hhcno  23409  hhcnf  23410  adjvalval  23442  leop2  23629  leoptri  23641  mdbr2  23801  dmdbr2  23808  mddmd2  23814  cdj3lem3b  23945  toslub  24193  tosglb  24194  lmdvg  24340  subfacp1lem3  24870  subfacp1lem5  24872  dfrdg2  25425  eqeelen  25845  brbtwn2  25846  colinearalg  25851  axcgrid  25857  axsegconlem1  25858  ax5seglem4  25873  ax5seglem5  25874  axbtwnid  25880  axpasch  25882  axeuclidlem  25903  axcontlem2  25906  axcontlem4  25908  axcontlem7  25911  axcontlem12  25916  itg2gt0cn  26262  ftc1cnnc  26281  opnrebl  26325  lmclim2  26466  caures  26468  sstotbnd2  26485  rrnmet  26540  rrncmslem  26543  isdrngo3  26577  isidlc  26627  fnnfpeq0  26741  wepwsolem  27118  fnwe2lem2  27128  islnm2  27155  lindfmm  27276  islindf4  27287  islindf5  27288  caofcan  27519  swdeq  28218  cvrval2  30134  isat3  30167  iscvlat2N  30184  glbconN  30236  ltrneq  31008  cdlemefrs29clN  31258  cdlemefrs32fva  31259  cdleme32fva  31296  cdlemk33N  31768  cdlemk34  31769  cdlemkid3N  31792  cdlemkid4  31793  diaglbN  31915  dibglbN  32026  dihglbcpreN  32160  dihglblem6  32200  hdmap1eulem  32684  hdmap1eulemOLDN  32685  hdmapoc  32794  hlhilocv  32820
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555  df-ral 2712
  Copyright terms: Public domain W3C validator