Theorem r19.21aiv 1759

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)

Hypothesis

Ref	Expression
r19.21aiv.1	|- (ph -> (x e. A -> ps))

Assertion

Ref	Expression
r19.21aiv	|- (ph -> A.x e. A ps)

Distinct variable group:   ph,x

Proof of Theorem r19.21aiv

Step	Hyp	Ref	Expression
1		ax-17 1007	. 2 |- (ph -> A.xph)
2		r19.21aiv.1	. 2 |- (ph -> (x e. A -> ps))
3	1, 2	r19.21ai 1758	1 |- (ph -> A.x e. A ps)

Syntax hints:   -> wi 3   e. wcel 994  A.wral 1691

This theorem is referenced by:  r19.21aiva 1760  r19.21aivv 1766  r19.37av 1807  rzal 2409  trin 2764  class2seteq 2809  onmindif 3061  ralxfr 3122  ssorduni 3147  onmindif2 3169  suceloni 3170  limuni3 3206  ralxp 3301  dmxp 3419  dffun8 3645  eqfnfv 3909  eqfnfv2 3911  ffnfv 3942  abrexex 3974  isocnv 4010  isotr 4011  f1oiso 4018  onfununi 4209  tfrlem12 4223  tz7.48-2 4258  oaass 4331  omass 4347  oelim2 4358  omsmo 4397  en2d 4541  dom2d 4545  pw2en 4587  mapenlem2 4637  unblem4 4689  unbnn2 4691  iunfi 4712  supmaxlem 4731  suppr 4733  supsnALT 4735  elirrv 4741  trcl 4791  r1tr 4800  tz9.13 4809  scottex 4862  scott0 4863  aceq3 4879  aceq5lem5 4885  ac6lem 4900  kmlem4 4914  kmlem11 4921  numthlem 4929  uniimadom 4956  ondomon 5006  cardmin 5010  carduniima 5040  alephval2 5052  alephval3 5053  cfsuc 5065  genpcl 5265  ltexprlem5 5300  suplem1pr 5315  negeui 5509  receui 5853  lbinfm 6216  xrsupsslem 6244  xrinfmsslem 6245  supxrun 6253  supxrpnf 6256  supxrunb1 6257  supxrunb2 6258  uzind 6376  uzwo4OLD 6381  uzwo3lem1 6388  uzwo3lem2 6389  flval3 6438  uzwo 6582  uzwoOLD 6583  fsequb 6654  seq1rn2 6686  seqzeq 6750  seqzrn2 6751  recan 7108  cvg2i 7125  fsum1i 7208  fsumconst 7241  serzcl2 7252  climconst2 7298  2climnn 7305  2climnn0 7306  iserzshft2i 7310  climaddlem3 7319  climmullem8 7330  clim2serz 7337  iserzmulc1 7339  iserzcmp 7345  climabslem 7351  climubii 7356  climsupi 7358  climcaui 7359  caucvgi 7366  serzf0i 7372  ser1clim0 7376  isumrecl 7414  reccnv 7422  expcnv 7437  cvgratlem5 7459  fsum0diag2 7464  fsum0diag4 7466  reeftlcl 7585  effsumlei 7605  efcn 7631  unbenlem 7716  infxpidmlem7 7770  unctb 7789  tgcl 7836  bastop1 7854  subbas 7856  indistop 7860  distop 7861  neif 7925  unnei 7945  cnpco 7979  cncnplem4 7987  cnconst 7990  bl2in 8053  metcnp 8098  tgioo 8126  lmconst 8145  lmuni 8162  lmfexlem3 8169  metelcls 8176  xplm 8186  lmcau 8207  bcthlem22 8231  bcthlem28 8237  grprlidrid 8270  grplactf1o 8339  vacnlem3 8584  nmoubi 8689  nmobndi 8692  blocni 8720  ip2eqi 8773  ubthlem13 8800  ubthlem13OLD 8801  ubthlem14 8802  hial2eq 9248  hlim0 9381  ocsh 9432  occon 9436  projlem26 9487  projlem29 9490  projlem31 9492  pjthlem14 9508  pjtheui 9511  shintcli 9569  hsupss 9585  spanss 9594  osumlem5 9860  nmopub 10112  nmfnleub 10129  nmcopexlem6 10235  nmcfnexlem6 10264  pjnmopi 10355  pjss2coi 10372  pjnormssi 10376  pjclem4 10408  pj3si 10416  pj3cor1i 10418  strlem3a 10460  strbi 10466  hstrlem3a 10468  hstrbi 10474  spansncv2 10501  ssmd1 10519  mdsl1i 10529  cvmdi 10532  mdexchi 10543  h1da 10557  chrelat2i 10573  mdsymlem6 10617  sumdmdii 10624  dmdbr5ati 10631  cayleylem2 10695  ref3w 10772  pospos 10882  toplat 10884  unmnd 10951  zrdivrng 10969  mapdiscn 11014  mapudiscn 11015  sallnei 11016  hmeogrp 11044  eqindhome 11047  qusp 11068  idfisf 11295  idsubfun 11312  fiuni 11420  fictb 11423  ordiso 11426  ordtypelem6 11432  ordtypelem7 11433  omsublim 11448  infenomsub 11450  omsubinit 11451  ntruni 11464  clsint2 11466  opnnei 11469  cnpnei 11472  cptclsscpt 11489  uncomp 11490  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  cncomp 11494  alexsublem1 11496  alexsublem2 11497  alexsublem3 11498  alexsub 11500  reconnlem3 11509  reconnlem5 11511  2ndc1stc 11538  2ndcctbss 11539  fneint 11547  reftr 11558  topfneec 11562  fnessref 11564  refssfne 11565  finptfin 11568  finlocfin 11570  lfinpfin 11574  locfincomp 11575  locfindsc 11576  comppfsc 11578  neibastop1 11579  neibastop2lem2 11581  neibastop2lem3 11582  neibastop2lem4 11583  topmtcl 11586  topmeet 11587  topjoin 11588  fnemeet1 11589  fnemeet2 11590  fnejoin1 11591  fnejoin2 11592  filrn 11643  neifg 11644  supfil 11645  filssufillem 11655  uffixfr 11660  fixufil 11661  ufinffr 11663  cnpfillim 11686  elfilmap 11690  fmf 11693  fmbas 11694  filmapss 11696  rnelfm 11699  fmfnfm 11704  fmufil 11705  sfcls 11716  flimfcls 11725  fcluscnplem 11729  fcluscomplem 11732  fcluscomp 11733  tailmap 11759  tailuni 11761  gaid 11776  gapm 11784  ralun 11789  findcard 11836  fimax 11837  frinfm 11850  sdclem2 11876  sdc 11877  seqpo 11878  metsstop 11909  cnimass 11949  cnresima 11952  txuni 11975  uptx 11978  sstotbnd 11992  ismtyhmeolem 12006  heiborlem16 12026  heiborlem19 12029  rrnmet 12072  rrntotbnd 12078  iccbnd 12082  phtpyco 12098  hgrablkne0 12199  hgrablkcard 12200

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011

This theorem depends on definitions:  df-bi 145  df-ral 1695

Copyright terms: Public domain