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

Theorem ralbidva 2665
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 1626 . 2  |-  F/ x ph
2 ralbidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2ralbida 2663 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    e. wcel 1717   A.wral 2649
This theorem is referenced by:  raleqbidva  2861  ordunisssuc  4624  tfindsg2  4781  poinxp  4881  soinxp  4882  frinxp  4883  funimass3  5785  fnsuppres  5891  cocan1  5963  cocan2  5964  isores2  5992  isoini2  5998  f1oweALT  6013  ofrfval  6252  ofrfval2  6262  dfsmo2  6545  smores  6550  smores2  6552  ac6sfi  7287  fimaxg  7290  ordunifi  7293  isfinite2  7301  fipreima  7347  supisolem  7408  ordiso2  7417  ordtypelem7  7426  cantnf  7582  wemapwe  7587  rankval3b  7685  rankonidlem  7687  iscard  7795  acndom  7865  dfac12lem3  7958  kmlem2  7964  cflim2  8076  cfsmolem  8083  ttukeylem6  8327  alephreg  8390  suplem2pr  8863  axsup  9084  sup3  9897  infm3  9899  suprleub  9904  dfinfmr  9917  infmrgelb  9920  ofsubeq0  9929  ofsubge0  9931  zextlt  10276  prime  10282  indstr  10477  supxr2  10824  supxrbnd1  10832  supxrbnd2  10833  supxrleub  10837  supxrbnd  10839  infmxrgelb  10845  fzshftral  11064  clim  12215  rlim  12216  clim2  12225  clim2c  12226  clim0c  12228  ello1mpt  12242  lo1o1  12253  o1lo1  12258  climabs0  12306  o1compt  12308  rlimdiv  12366  geomulcvg  12580  mertenslem2  12589  mertens  12590  rpnnen2  12752  sqr2irr  12775  pc11  13180  pcz  13181  1arith  13222  vdwlem8  13283  vdwlem11  13286  vdw  13289  ramval  13303  pwsle  13641  mrieqvd  13790  mreacs  13810  cidpropd  13863  ismon2  13887  monpropd  13890  isepi  13893  isepi2  13894  subsubc  13977  funcres2b  14021  funcpropd  14024  isfull2  14035  isfth2  14039  fucsect  14096  fucinv  14097  pospropd  14488  ipodrsfi  14516  tsrss  14582  mndpropd  14648  grpidpropd  14649  grppropd  14750  issubg4  14888  gass  15005  gexdvds  15145  gexdvds2  15146  subgpgp  15158  sylow3lem6  15193  efgval2  15283  efgsp1  15296  dprdf11  15508  subgdmdprd  15519  rngpropd  15622  abvpropd  15857  lsspropd  16020  lbspropd  16098  assapropd  16313  psrbaglefi  16364  psrbagconf1o  16366  gsumbagdiaglem  16367  mplmonmul  16454  phlpropd  16809  ishil2  16869  tgss2  16975  isclo  17074  neips  17100  opnnei  17107  isperf3  17139  ssidcn  17241  lmbrf  17246  cnnei  17268  cnrest2  17272  lmss  17284  lmres  17286  ist1-2  17333  ist1-3  17335  isreg2  17363  cmpfi  17393  1stccn  17447  subislly  17465  kgencn  17509  ptclsg  17568  ptcnplem  17574  xkococnlem  17612  xkoinjcn  17640  tgqtop  17665  qtopcn  17667  fbflim  17929  flimrest  17936  flfnei  17944  isflf  17946  cnflf  17955  fclsopn  17967  fclsbas  17974  fclsrest  17977  isfcf  17987  cnfcf  17995  ptcmplem3  18006  tmdgsum2  18047  eltsms  18083  tsmsgsum  18089  tsmssubm  18093  tsmsf1o  18095  utopsnneiplem  18198  ismet2  18272  prdsxmetlem  18306  elmopn2  18365  prdsbl  18411  metss  18428  metrest  18444  metcnp  18461  metcnp2  18462  metcn  18463  metucn  18490  nrginvrcn  18598  metdsge  18750  divcn  18769  elcncf2  18791  mulc1cncf  18806  cncfmet  18809  evth2  18856  lmmbr2  19083  lmmbrf  19086  iscfil2  19090  cfil3i  19093  iscau2  19101  iscau4  19103  iscauf  19104  caucfil  19107  iscmet3lem3  19114  cfilres  19120  causs  19122  lmclim  19126  evthicc2  19224  cniccbdd  19225  ovolfioo  19231  ovolficc  19232  ismbl2  19290  mbfsup  19423  mbfinf  19424  mbflimsup  19425  0plef  19431  mbfi1flim  19482  xrge0f  19490  itg2mulclem  19505  itgeqa  19572  ellimc2  19631  ellimc3  19633  limcflf  19635  cnlimc  19642  dvferm1  19736  dvferm2  19738  rolle  19741  dvivthlem1  19759  ftc1lem6  19792  itgsubst  19800  mdegle0  19867  deg1leb  19885  plydivex  20081  ulm2  20168  ulmcaulem  20177  ulmcau  20178  ulmdvlem3  20185  abelthlem9  20223  abelth  20224  rlimcnp  20671  ftalem3  20724  issqf  20786  sqf11  20789  dvdsmulf1o  20846  dchrelbas4  20894  dchrinv  20912  2sqlem6  21020  chpo1ubb  21042  dchrmusumlema  21054  dchrisum0lema  21075  ostth3  21199  isgrpo2  21633  nmounbi  22125  blocnilem  22153  isph  22171  phoeqi  22207  h2hcau  22330  h2hlm  22331  hial2eq2  22457  hoeq1  23181  hoeq2  23182  adjsym  23184  cnvadj  23243  hhcno  23255  hhcnf  23256  adjvalval  23288  leop2  23475  leoptri  23487  mdbr2  23647  dmdbr2  23654  mddmd2  23660  cdj3lem3b  23791  lmdvg  24142  subfacp1lem3  24647  subfacp1lem5  24649  dfrdg2  25176  tfrALTlem  25300  eqeelen  25557  brbtwn2  25558  colinearalg  25563  axcgrid  25569  axsegconlem1  25570  ax5seglem4  25585  ax5seglem5  25586  axbtwnid  25592  axpasch  25594  axeuclidlem  25615  axcontlem2  25618  axcontlem4  25620  axcontlem7  25623  axcontlem12  25628  itg2gt0cn  25960  ftc1cnnc  25979  opnrebl  26014  lmclim2  26155  caures  26157  sstotbnd2  26174  rrnmet  26229  rrncmslem  26232  isdrngo3  26266  isidlc  26316  fnnfpeq0  26430  wepwsolem  26807  fnwe2lem2  26817  islnm2  26845  lindfmm  26966  islindf4  26977  islindf5  26978  caofcan  27209  cvrval2  29389  isat3  29422  iscvlat2N  29439  glbconN  29491  ltrneq  30263  cdlemefrs29clN  30513  cdlemefrs32fva  30514  cdleme32fva  30551  cdlemk33N  31023  cdlemk34  31024  cdlemkid3N  31047  cdlemkid4  31048  diaglbN  31170  dibglbN  31281  dihglbcpreN  31415  dihglblem6  31455  hdmap1eulem  31939  hdmap1eulemOLDN  31940  hdmapoc  32049  hlhilocv  32075
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2654
  Copyright terms: Public domain W3C validator