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

Theorem ralrimiv 2625
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 1605 . 2  |-  F/ x ph
2 ralrimiv.1 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
31, 2ralrimi 2624 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   A.wral 2543
This theorem is referenced by:  ralrimiva  2626  ralrimivw  2627  ralrimivv  2634  r19.27av  2681  rr19.3v  2909  rabssdv  3253  rzal  3555  trin  4123  class2seteq  4179  onmindif  4482  ralxfrALT  4553  ssorduni  4577  onminex  4598  onmindif2  4603  suceloni  4604  limuni3  4643  issref  5056  frxp  6225  poxp  6227  onfununi  6358  onnseq  6361  tfrlem12  6405  tz7.48-2  6454  oaass  6559  omass  6578  oelim2  6593  oelimcl  6598  oaabs2  6643  omabs  6645  undifixp  6852  dom2lem  6901  isinf  7076  unblem4  7112  unbnn2  7114  marypha1lem  7186  supiso  7223  ordiso2  7230  card2inf  7269  elirrv  7311  wemapwe  7400  trcl  7410  tz9.13  7463  rankval3b  7498  rankunb  7522  rankuni2b  7525  scott0  7556  dfac8alem  7656  carduniima  7723  alephsmo  7729  alephval3  7737  iunfictbso  7741  dfac3  7748  dfac5lem5  7754  dfac12r  7772  dfac12k  7773  kmlem4  7779  kmlem11  7786  cfsuc  7883  cofsmo  7895  cfsmolem  7896  coftr  7899  alephsing  7902  infpssrlem3  7931  fin23lem30  7968  isf32lem2  7980  isf32lem3  7981  isf34lem6  8006  fin1a2lem11  8036  fin1a2lem13  8038  fin1a2s  8040  axcc2lem  8062  domtriomlem  8068  axdc3lem2  8077  axdc4lem  8081  axcclem  8083  axdclem2  8147  iundom2g  8162  uniimadom  8166  cardmin  8186  alephval2  8194  alephreg  8204  fpwwe2lem12  8263  wunex2  8360  wuncval2  8369  tskwe2  8395  inar1  8397  tskuni  8405  gruun  8428  intgru  8436  grutsk1  8443  genpcl  8632  ltexprlem5  8664  suplem1pr  8676  supexpr  8678  supsrlem  8733  axpre-sup  8791  supmul1  9719  supmullem1  9720  supmul  9722  peano5nni  9749  uzind  10103  zindd  10113  uzwo  10281  uzwoOLD  10282  lbzbi  10306  xrsupsslem  10625  xrinfmsslem  10626  supxrun  10634  supxrpnf  10637  supxrunb1  10638  supxrunb2  10639  icoshftf1o  10759  flval3  10945  axdc4uzlem  11044  sqrlem1  11728  sqrlem6  11733  fsum0diag2  12245  alzdvds  12578  gcdcllem1  12690  maxprmfct  12792  unbenlem  12955  vdwlem6  13033  vdwlem10  13037  firest  13337  mrieqv2d  13541  iscatd  13575  setcmon  13919  setcepi  13920  isglbd  14221  isacs4lem  14271  acsfiindd  14280  acsmapd  14281  psss  14323  ghmrn  14696  ghmpreima  14704  cntz2ss  14808  lsmsubg  14965  efgsfo  15048  gsumzaddlem  15203  dmdprdd  15237  dprd2da  15277  imasrng  15402  isabvd  15585  issrngd  15626  islssd  15693  lbsextlem3  15913  lbsextlem4  15914  lidldvgen  16007  isphld  16558  tgcl  16707  distop  16733  indistopon  16738  pptbas  16745  toponmre  16830  opnnei  16857  neiuni  16859  neindisj2  16860  ordtrest2  16934  cnpnei  16993  cnindis  17020  cmpcld  17129  uncmp  17130  hauscmplem  17133  2ndc1stc  17177  1stcrest  17179  1stcelcls  17187  llyrest  17211  nllyrest  17212  cldllycmp  17221  txcls  17299  ptpjcn  17305  ptclsg  17309  dfac14lem  17311  xkoccn  17313  txlly  17330  txnlly  17331  ptrescn  17333  tx1stc  17344  xkoco1cn  17351  xkoco2cn  17352  xkococn  17354  xkoinjcn  17381  qtopeu  17407  hmeofval  17449  ordthmeolem  17492  isfild  17553  fbasrn  17579  trfil2  17582  flimclslem  17679  fclsrest  17719  fclscf  17720  flimfcls  17721  alexsubALTlem1  17741  alexsubALTlem2  17742  alexsubALTlem3  17743  alexsubALT  17745  divstgpopn  17802  isxmetd  17891  imasdsf1olem  17937  blcls  18052  prdsxmslem2  18075  dscmet  18095  nrmmetd  18097  reperflem  18323  reconnlem2  18332  xrge0tsms  18339  fsumcn  18374  cnheibor  18453  tchcph  18667  lmmbr  18684  caubl  18733  ivthlem1  18811  ovolctb  18849  ovoliunlem2  18862  ovolscalem1  18872  ovolicc2  18881  voliunlem3  18909  ismbfd  18995  mbfimaopnlem  19010  itg2le  19094  ellimc2  19227  c1liplem1  19343  plyeq0lem  19592  dgreq0  19646  aannenlem1  19708  pilem2  19828  cxpcn3lem  20087  scvxcvx  20280  musum  20431  dchrisum0flb  20659  ostth2lem2  20783  htthlem  21497  ocsh  21862  shintcli  21908  pjss2coi  22744  pjnormssi  22748  pjclem4  22779  pj3si  22787  pj3cor1i  22789  strlem3a  22832  strb  22838  hstrlem3a  22840  hstrbi  22846  spansncv2  22873  mdsl1i  22901  cvmdi  22904  mdexchi  22915  h1da  22929  mdsymlem6  22988  sumdmdii  22995  dmdbr5ati  23002  ballotlemimin  23064  rnmpt2ss  23239  supssd  23248  disjabrex  23359  disjabrexf  23360  lmdvg  23376  xrge0tsmsd  23382  pwsiga  23491  measiun  23545  cntmeas  23553  probmeasb  23633  erdszelem8  23729  cvmsss2  23805  cvmfolem  23810  eupap1  23900  rtrclreclem.min  24044  dfrtrcl2  24045  dfon2lem8  24146  dfon2lem9  24147  dfon2  24148  rdgprc  24151  trpredtr  24233  trpredmintr  24234  trpredelss  24235  dftrpred3g  24236  trpredpo  24238  trpredrec  24241  wfrlem15  24270  frr3g  24280  frrlem5b  24286  frrlem5d  24288  sltval2  24310  funpartfv  24483  uncum2  25110  eqfnung2  25118  repfuntw  25160  prl1  25168  prl2  25169  dstr  25171  supwlub  25274  toplat  25290  sallnei  25529  intopcoaconlem3b  25538  intopcoaconb  25540  qusp  25542  cmptdst  25568  limptlimpr2lem2  25575  lvsovso  25626  claddrvr  25648  sigadd  25649  issubrv  25672  subclrvd  25674  clsmulcv  25682  clsmulrv  25683  idsubfun  25858  cmpmor  25975  setiscat  25979  indcls2  25996  nn0prpwlem  26238  ntruni  26245  clsint2  26247  fneint  26277  reftr  26289  fnessref  26293  refssfne  26294  locfincf  26306  comppfsc  26307  neibastop1  26308  neibastop2lem  26309  sdclem2  26452  fdc  26455  seqpo  26457  prdsbnd  26517  heibor  26545  rrnequiv  26559  0idl  26650  intidl  26654  unichnidl  26656  prnc  26692  pellfundre  26966  pellfundge  26967  pellfundlb  26969  dford3lem1  27119  aomclem2  27152  frlmsslsp  27248  psgnunilem2  27418  psgnghm  27437  hashgcdeq  27517  addrcom  27680  stoweidlem35  27784  funressnfv  27991  tz6.12-afv  28035  nbusgra  28143  nbgra0nb  28144  nbgra0edg  28147  uvtxnbgravtx  28167  bnj518  28918  bnj1137  29025  bnj1136  29027  bnj1413  29065  bnj1417  29071  bnj60  29092  lsmcv2  29219  lcvexchlem4  29227  lcvexchlem5  29228  eqlkr  29289  paddclN  30031  pclfinN  30089  ldilcnv  30304  ldilco  30305  cdleme25dN  30545  cdlemj2  31011  tendocan  31013  erng1lem  31176  erngdvlem4-rN  31188  dihord2pre  31415  dihglblem2N  31484  dochvalr  31547  hdmap14lem12  32072  hdmap14lem13  32073
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-nf 1532  df-ral 2548
  Copyright terms: Public domain W3C validator