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

Theorem ralrimiv 2627
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.)
Hypothesis
Ref Expression
ralrimiv.1  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
Assertion
Ref Expression
ralrimiv  |-  ( ph  ->  A. x  e.  A  ps )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    A( x)

Proof of Theorem ralrimiv
StepHypRef Expression
1 nfv 1606 . 2  |-  F/ x ph
2 ralrimiv.1 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
31, 2ralrimi 2626 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1685   A.wral 2545
This theorem is referenced by:  ralrimiva  2628  ralrimivw  2629  ralrimivv  2636  r19.27av  2683  rr19.3v  2911  rabssdv  3255  rzal  3557  trin  4125  class2seteq  4179  onmindif  4482  ralxfrALT  4553  ssorduni  4577  onminex  4598  onmindif2  4603  suceloni  4604  limuni3  4643  issref  5056  frxp  6187  poxp  6189  onfununi  6354  onnseq  6357  tfrlem12  6401  tz7.48-2  6450  oaass  6555  omass  6574  oelim2  6589  oelimcl  6594  oaabs2  6639  omabs  6641  undifixp  6848  dom2lem  6897  isinf  7072  unblem4  7108  unbnn2  7110  marypha1lem  7182  supiso  7219  ordiso2  7226  card2inf  7265  elirrv  7307  wemapwe  7396  trcl  7406  tz9.13  7459  rankval3b  7494  rankunb  7518  rankuni2b  7521  scott0  7552  dfac8alem  7652  carduniima  7719  alephsmo  7725  alephval3  7733  iunfictbso  7737  dfac3  7744  dfac5lem5  7750  dfac12r  7768  dfac12k  7769  kmlem4  7775  kmlem11  7782  cfsuc  7879  cofsmo  7891  cfsmolem  7892  coftr  7895  alephsing  7898  infpssrlem3  7927  fin23lem30  7964  isf32lem2  7976  isf32lem3  7977  isf34lem6  8002  fin1a2lem11  8032  fin1a2lem13  8034  fin1a2s  8036  axcc2lem  8058  domtriomlem  8064  axdc3lem2  8073  axdc4lem  8077  axcclem  8079  axdclem2  8143  iundom2g  8158  uniimadom  8162  cardmin  8182  alephval2  8190  alephreg  8200  fpwwe2lem12  8259  wunex2  8356  wuncval2  8365  tskwe2  8391  inar1  8393  tskuni  8401  gruun  8424  intgru  8432  grutsk1  8439  genpcl  8628  ltexprlem5  8660  suplem1pr  8672  supexpr  8674  supsrlem  8729  axpre-sup  8787  supmul1  9715  supmullem1  9716  supmul  9718  peano5nni  9745  uzind  10099  zindd  10109  uzwo  10277  uzwoOLD  10278  lbzbi  10302  xrsupsslem  10620  xrinfmsslem  10621  supxrun  10629  supxrpnf  10632  supxrunb1  10633  supxrunb2  10634  icoshftf1o  10754  flval3  10940  axdc4uzlem  11039  sqrlem1  11723  sqrlem6  11728  fsum0diag2  12240  alzdvds  12573  gcdcllem1  12685  maxprmfct  12787  unbenlem  12950  vdwlem6  13028  vdwlem10  13032  firest  13332  mrieqv2d  13536  iscatd  13570  setcmon  13914  setcepi  13915  isglbd  14216  isacs4lem  14266  acsfiindd  14275  acsmapd  14276  psss  14318  ghmrn  14691  ghmpreima  14699  cntz2ss  14803  lsmsubg  14960  efgsfo  15043  gsumzaddlem  15198  dmdprdd  15232  dprd2da  15272  imasrng  15397  isabvd  15580  issrngd  15621  islssd  15688  lbsextlem3  15908  lbsextlem4  15909  lidldvgen  16002  isphld  16553  tgcl  16702  distop  16728  indistopon  16733  pptbas  16740  toponmre  16825  opnnei  16852  neiuni  16854  neindisj2  16855  ordtrest2  16929  cnpnei  16988  cnindis  17015  cmpcld  17124  uncmp  17125  hauscmplem  17128  2ndc1stc  17172  1stcrest  17174  1stcelcls  17182  llyrest  17206  nllyrest  17207  cldllycmp  17216  txcls  17294  ptpjcn  17300  ptclsg  17304  dfac14lem  17306  xkoccn  17308  txlly  17325  txnlly  17326  ptrescn  17328  tx1stc  17339  xkoco1cn  17346  xkoco2cn  17347  xkococn  17349  xkoinjcn  17376  qtopeu  17402  hmeofval  17444  ordthmeolem  17487  isfild  17548  fbasrn  17574  trfil2  17577  flimclslem  17674  fclsrest  17714  fclscf  17715  flimfcls  17716  alexsubALTlem1  17736  alexsubALTlem2  17737  alexsubALTlem3  17738  alexsubALT  17740  divstgpopn  17797  isxmetd  17886  imasdsf1olem  17932  blcls  18047  prdsxmslem2  18070  dscmet  18090  nrmmetd  18092  reperflem  18318  reconnlem2  18327  xrge0tsms  18334  fsumcn  18369  cnheibor  18448  tchcph  18662  lmmbr  18679  caubl  18728  ivthlem1  18806  ovolctb  18844  ovoliunlem2  18857  ovolscalem1  18867  ovolicc2  18876  voliunlem3  18904  ismbfd  18990  mbfimaopnlem  19005  itg2le  19089  ellimc2  19222  c1liplem1  19338  plyeq0lem  19587  dgreq0  19641  aannenlem1  19703  pilem2  19823  cxpcn3lem  20082  scvxcvx  20275  musum  20426  dchrisum0flb  20654  ostth2lem2  20778  htthlem  21490  ocsh  21855  shintcli  21901  pjss2coi  22737  pjnormssi  22741  pjclem4  22772  pj3si  22780  pj3cor1i  22782  strlem3a  22825  strb  22831  hstrlem3a  22833  hstrbi  22839  spansncv2  22866  mdsl1i  22894  cvmdi  22897  mdexchi  22908  h1da  22922  mdsymlem6  22981  sumdmdii  22988  dmdbr5ati  22995  ballotlemimin  23058  erdszelem8  23134  cvmsss2  23210  cvmfolem  23215  eupap1  23305  rtrclreclem.min  23449  dfrtrcl2  23450  dfon2lem8  23548  dfon2lem9  23549  dfon2  23550  rdgprc  23553  trpredtr  23635  trpredmintr  23636  trpredelss  23637  dftrpred3g  23638  trpredpo  23640  trpredrec  23643  wfrlem15  23672  frr3g  23682  frrlem5b  23688  frrlem5d  23690  sltval2  23711  axfelem20  23767  axfelem21  23768  funpartfv  23891  uncum2  24509  eqfnung2  24518  repfuntw  24560  prl1  24568  prl2  24569  dstr  24571  supwlub  24674  toplat  24690  sallnei  24929  intopcoaconlem3b  24938  intopcoaconb  24940  qusp  24942  cmptdst  24968  limptlimpr2lem2  24975  lvsovso  25026  claddrvr  25048  sigadd  25049  issubrv  25072  subclrvd  25074  clsmulcv  25082  clsmulrv  25083  idsubfun  25258  cmpmor  25375  setiscat  25379  indcls2  25396  nn0prpwlem  25638  ntruni  25645  clsint2  25647  fneint  25677  reftr  25689  fnessref  25693  refssfne  25694  locfincf  25706  comppfsc  25707  neibastop1  25708  neibastop2lem  25709  sdclem2  25852  fdc  25855  seqpo  25857  prdsbnd  25917  heibor  25945  rrnequiv  25959  0idl  26050  intidl  26054  unichnidl  26056  prnc  26092  pellfundre  26366  pellfundge  26367  pellfundlb  26369  dford3lem1  26519  aomclem2  26552  frlmsslsp  26648  psgnunilem2  26818  psgnghm  26837  hashgcdeq  26917  addrcom  27080  stoweidlem35  27184  funressnfv  27371  tz6.12-afv  27415  bnj518  28186  bnj1137  28293  bnj1136  28295  bnj1413  28333  bnj1417  28339  bnj60  28360  lsmcv2  28487  lcvexchlem4  28495  lcvexchlem5  28496  eqlkr  28557  paddclN  29299  pclfinN  29357  ldilcnv  29572  ldilco  29573  cdleme25dN  29813  cdlemj2  30279  tendocan  30281  erng1lem  30444  erngdvlem4-rN  30456  dihord2pre  30683  dihglblem2N  30752  dochvalr  30815  hdmap14lem12  31340  hdmap14lem13  31341
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-11 1716
This theorem depends on definitions:  df-bi 179  df-nf 1533  df-ral 2550
  Copyright terms: Public domain W3C validator