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

Theorem ralrimiv 2780
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 1629 . 2  |-  F/ x ph
2 ralrimiv.1 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
31, 2ralrimi 2779 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   A.wral 2697
This theorem is referenced by:  ralrimiva  2781  ralrimivw  2782  ralrimivv  2789  r19.27av  2836  rr19.3v  3069  rabssdv  3415  rzal  3721  trin  4304  class2seteq  4360  onmindif  4662  ralxfrALT  4733  ssorduni  4757  onminex  4778  onmindif2  4783  suceloni  4784  limuni3  4823  issref  5238  fnpr  5941  fnprOLD  5942  frxp  6447  poxp  6449  onfununi  6594  onnseq  6597  tfrlem12  6641  tz7.48-2  6690  oaass  6795  omass  6814  oelim2  6829  oelimcl  6834  oaabs2  6879  omabs  6881  undifixp  7089  dom2lem  7138  isinf  7313  unblem4  7353  unbnn2  7355  marypha1lem  7429  supiso  7466  ordiso2  7473  card2inf  7512  elirrv  7554  wemapwe  7643  trcl  7653  tz9.13  7706  rankval3b  7741  rankunb  7765  rankuni2b  7768  scott0  7799  dfac8alem  7899  carduniima  7966  alephsmo  7972  alephval3  7980  iunfictbso  7984  dfac3  7991  dfac5lem5  7997  dfac12r  8015  dfac12k  8016  kmlem4  8022  kmlem11  8029  cfsuc  8126  cofsmo  8138  cfsmolem  8139  coftr  8142  alephsing  8145  infpssrlem3  8174  fin23lem30  8211  isf32lem2  8223  isf32lem3  8224  isf34lem6  8249  fin1a2lem11  8279  fin1a2lem13  8281  fin1a2s  8283  axcc2lem  8305  domtriomlem  8311  axdc3lem2  8320  axdc4lem  8324  axcclem  8326  axdclem2  8389  iundom2g  8404  uniimadom  8408  cardmin  8428  alephval2  8436  alephreg  8446  fpwwe2lem12  8505  wunex2  8602  wuncval2  8611  tskwe2  8637  inar1  8639  tskuni  8647  gruun  8670  intgru  8678  grutsk1  8685  genpcl  8874  ltexprlem5  8906  suplem1pr  8918  supexpr  8920  supsrlem  8975  axpre-sup  9033  supmul1  9962  supmullem1  9963  supmul  9965  peano5nni  9992  uzind  10350  zindd  10360  uzwo  10528  uzwoOLD  10529  lbzbi  10553  xrsupsslem  10874  xrinfmsslem  10875  supxrun  10883  supxrpnf  10886  supxrunb1  10887  supxrunb2  10888  icoshftf1o  11009  flval3  11210  axdc4uzlem  11309  sqrlem1  12036  sqrlem6  12041  fsum0diag2  12554  alzdvds  12887  gcdcllem1  12999  maxprmfct  13101  unbenlem  13264  vdwlem6  13342  vdwlem10  13346  firest  13648  mrieqv2d  13852  iscatd  13886  setcmon  14230  setcepi  14231  isglbd  14532  isacs4lem  14582  acsfiindd  14591  acsmapd  14592  psss  14634  ghmrn  15007  ghmpreima  15015  cntz2ss  15119  lsmsubg  15276  efgsfo  15359  gsumzaddlem  15514  dmdprdd  15548  dprd2da  15588  imasrng  15713  isabvd  15896  issrngd  15937  islssd  16000  lbsextlem3  16220  lbsextlem4  16221  lidldvgen  16314  isphld  16873  tgcl  17022  distop  17048  indistopon  17053  pptbas  17060  toponmre  17145  opnnei  17172  neiuni  17174  neindisj2  17175  ordtrest2  17256  cnpnei  17316  cnindis  17344  cmpcld  17453  uncmp  17454  hauscmplem  17457  2ndc1stc  17502  1stcrest  17504  1stcelcls  17512  llyrest  17536  nllyrest  17537  cldllycmp  17546  txcls  17624  ptpjcn  17631  ptclsg  17635  dfac14lem  17637  xkoccn  17639  txlly  17656  txnlly  17657  ptrescn  17659  tx1stc  17670  xkoco1cn  17677  xkoco2cn  17678  xkococn  17680  xkoinjcn  17707  qtopeu  17736  hmeofval  17778  ordthmeolem  17821  isfild  17878  fbasrn  17904  trfil2  17907  flimclslem  18004  fclsrest  18044  fclscf  18045  flimfcls  18046  alexsubALTlem1  18066  alexsubALTlem2  18067  alexsubALTlem3  18068  alexsubALT  18070  divstgpopn  18137  isxmetd  18344  imasdsf1olem  18391  blcls  18524  prdsxmslem2  18547  metustfbasOLD  18583  metustfbas  18584  dscmet  18608  nrmmetd  18610  reperflem  18837  reconnlem2  18846  xrge0tsms  18853  fsumcn  18888  cnheibor  18968  tchcph  19182  lmmbr  19199  caubl  19248  ivthlem1  19336  ovolctb  19374  ovoliunlem2  19387  ovolscalem1  19397  ovolicc2  19406  voliunlem3  19434  ismbfd  19520  mbfimaopnlem  19535  itg2le  19619  ellimc2  19752  c1liplem1  19868  plyeq0lem  20117  dgreq0  20171  aannenlem1  20233  pilem2  20356  cxpcn3lem  20619  scvxcvx  20812  musum  20964  dchrisum0flb  21192  ostth2lem2  21316  usgrares1  21412  nbusgra  21428  nbgra0nb  21429  nbgra0edg  21432  cusgrafilem2  21477  usgrasscusgra  21480  uvtxnbgravtx  21492  fargshiftf  21611  fargshiftfva  21614  eupatrl  21678  eupap1  21686  htthlem  22408  ocsh  22773  shintcli  22819  pjss2coi  23655  pjnormssi  23659  pjclem4  23690  pj3si  23698  pj3cor1i  23700  strlem3a  23743  strb  23749  hstrlem3a  23751  hstrbi  23757  spansncv2  23784  mdsl1i  23812  cvmdi  23815  mdexchi  23826  h1da  23840  mdsymlem6  23899  sumdmdii  23906  dmdbr5ati  23913  isoun  24077  supssd  24086  xrge0tsmsd  24211  pwsiga  24501  measiun  24560  dya2iocuni  24621  erdszelem8  24872  cvmsss2  24949  cvmfolem  24954  rtrclreclem.min  25135  dfrtrcl2  25136  dfon2lem8  25401  dfon2lem9  25402  dfon2  25403  rdgprc  25406  trpredtr  25488  trpredmintr  25489  trpredelss  25490  dftrpred3g  25491  trpredpo  25493  trpredrec  25496  wfrlem15  25525  frr3g  25535  frrlem5b  25541  frrlem5d  25543  sltval2  25565  supaddc  26184  supadd  26185  mblfinlem  26190  nn0prpwlem  26262  ntruni  26267  clsint2  26269  fneint  26294  reftr  26306  fnessref  26310  refssfne  26311  locfincf  26323  comppfsc  26324  neibastop1  26325  neibastop2lem  26326  sdclem2  26383  fdc  26386  seqpo  26388  prdsbnd  26439  heibor  26467  rrnequiv  26481  0idl  26572  intidl  26576  unichnidl  26578  prnc  26614  pellfundre  26881  pellfundge  26882  pellfundlb  26884  dford3lem1  27034  aomclem2  27067  frlmsslsp  27163  psgnunilem2  27333  psgnghm  27352  hashgcdeq  27432  addrcom  27594  funressnfv  27906  tz6.12-afv  27951  otiunsndisj  28002  shwrdeqrep  28160  3cyclfrgrarn  28261  iunconlem2  28902  bnj518  29111  bnj1137  29218  bnj1136  29220  bnj1413  29258  bnj1417  29264  bnj60  29285  lsmcv2  29666  lcvexchlem4  29674  lcvexchlem5  29675  eqlkr  29736  paddclN  30478  pclfinN  30536  ldilcnv  30751  ldilco  30752  cdleme25dN  30992  cdlemj2  31458  tendocan  31460  erng1lem  31623  erngdvlem4-rN  31635  dihord2pre  31862  dihglblem2N  31931  dochvalr  31994  hdmap14lem12  32519  hdmap14lem13  32520
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554  df-ral 2702
  Copyright terms: Public domain W3C validator