Theorem r19.21aiv 2175

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 1317	. 2 |- (ph -> A.xph)
2		r19.21aiv.1	. 2 |- (ph -> (x e. A -> ps))
3	1, 2	r19.21ai 2174	1 |- (ph -> A.x e. A ps)

Syntax hints:   -> wi 3   e. wcel 1300  A.wral 2105

This theorem is referenced by:  r19.21aiva 2176  r19.21aivv 2183  r19.27av 2224  r19.37av 2233  rzal 2970  rzalOLD 2971  trin 3422  class2seteq 3472  onmindif 3760  eufromeq6 3833  ralxfr 3839  ssorduni 3870  ssorduniOLD 3871  onmindif2 3893  suceloni 3894  limuni3 3936  ralxp 4041  dmxp 4177  dmxpOLD 4178  dffun8OLD 4449  nfunsnOLD 4707  eqfnfv 4766  ffnfv 4801  abrexex 4836  isocnv 4873  isotr 4874  f1oiso 4881  onfununi 5116  tfrlem12 5130  tz7.48-2 5166  oaass 5243  omass 5259  oelim2 5270  omsmo 5314  en2d 5459  dom2d 5463  pw2en 5505  mapenlem2 5584  unblem4 5636  unbnn2 5638  iunfi 5659  supmaxlem 5678  suppr 5680  supsnALT 5682  ordiso 5683  ordtypelem6 5689  ordtypelem7 5690  elirrv 5700  trcl 5752  r1tr 5765  tz9.13 5774  scottex 5846  scott0 5847  omsublim 5887  infenomsub 5889  omsubinit 5890  aceq3 5895  aceq5lem5 5901  ac6lem 5916  kmlem4 5930  kmlem11 5937  numthlem 5945  uniimadom 5972  ondomon 6008  cardmin 6012  carduniima 6038  alephval2 6050  alephval3 6051  cfsuc 6063  genpcl 6263  ltexprlem5 6298  suplem1pr 6313  negeui 6510  receui 6890  lbinfm 7257  xrsupsslem 7285  xrinfmsslem 7286  supxrun 7294  supxrpnf 7297  supxrunb1 7298  supxrunb2 7299  uzind 7417  uzwo4OLD 7422  uzwo3lem1 7429  uzwo3lem2 7430  flval3 7479  uzwo 7624  uzwoOLD 7625  fsequb 7702  seq1rn2 7734  seqzeq 7798  seqzrn2 7799  recan 8157  cvg2i 8174  fsum1i 8265  fsumconst 8298  serzcl2 8309  climconst2 8355  2climnn 8362  2climnn0 8363  iserzshft2i 8367  climaddlem3 8376  climmullem8 8387  clim2serz 8394  iserzmulc1 8396  iserzcmp 8402  climabslem 8408  climubii 8413  climsupi 8415  climcaui 8416  caucvgi 8423  serzf0i 8429  ser1clim0 8433  isumrecl 8471  reccnv 8479  expcnv 8494  cvgratlem5 8516  fsum0diag2 8521  fsum0diag4 8523  reeftlcl 8642  effsumlei 8662  efcn 8688  unbenlem 8773  infxpidmlem7 8827  unctb 8846  tgcl 8894  bastop1 8912  subbas 8914  indistop 8918  distop 8919  txuni 8935  neif 8991  unnei 9011  cnpnei 9043  cnpco 9046  cncnplem4 9054  cnconst 9057  bl2in 9120  metcnp 9165  tgioo 9193  lmconst 9212  lmuni 9229  lmfexlem3 9236  metelcls 9243  xplm 9253  lmcau 9274  bcthlem22 9298  bcthlem28 9304  grprlidrid 9337  grplactf1o 9406  gaid 9454  gapm 9462  vacnlem3 9669  nmoubi 9774  nmobndi 9777  blocni 9805  ip2eqi 9858  ubthlem13 9885  ubthlem13OLD 9886  ubthlem14 9887  findcardOLD 10179  fiuni 10219  uptx 10226  filrn 10293  filmapss 10309  fmf 10310  fmbas 10311  elfilmap 10312  cncomp 10331  unmnd 10405  zrdivrng 10418  hial2eq 10605  hlim0 10738  ocsh 10789  occon 10793  projlem26 10844  projlem29 10847  projlem31 10849  pjthlem14 10865  pjtheui 10868  shintcli 10926  hsupss 10942  spanss 10951  osumlem5 11217  nmopub 11469  nmfnleub 11486  nmcopexlem6 11593  nmcfnexlem6 11622  pjnmopi 11719  pjss2coi 11736  pjnormssi 11740  pjclem4 11772  pj3si 11780  pj3cor1i 11782  strlem3a 11824  strb 11830  hstrlem3a 11832  hstrbi 11838  spansncv2 11865  ssmd1 11883  mdsl1i 11893  cvmdi 11896  mdexchi 11907  h1da 11921  chrelat2i 11937  mdsymlem6 11980  sumdmdii 11987  dmdbr5ati 11994  bnj1284 13482  bnj1280 13483  bnj1417 13530  bnj1440 13543  bnj1496 13559  seqzresval2 13616  cayleylem2 13642  lbzbi 13657  alzdvds 13695  gcdcllem1 13718  gcdcllem2 13719  dfon2lem8 13856  dfon2lem9 13857  dfon2 13858  frxp 13951  wfrlem15 13971  frr3g 13980  sltval2 13997  axfelem16 14046  axfelem17 14047  ref4w 14370  surrc2 14390  uncum2 14441  eqfnung2 14459  surjsec 14462  prmapcp2 14497  repfuntw 14502  repcpwti 14503  cbicplem 14508  unprj 14511  prl1 14513  prl2 14514  dstr 14516  suplub2 14616  pospos 14635  toplat 14638  fprod1i 14673  fprod1ib 14686  ltlga 14729  curgrpact 14735  mapdiscnlem 14870  mapudiscn 14872  sallnei 14873  hmeogrp 14892  eqindhome 14895  qusp 14908  istopx 14918  fbaslim2 14936  iscnp3 14946  cntrsetlem 14999  lvsovso 15038  lvsovso3 15040  dualalg 15131  dualcat2 15133  idfisf 15189  idsubfun 15206  intartar 15255  inttaror 15277  carinttar 15279  cartarlim 15282  fictb 15371  ordisoOLD 15374  ordtypelem6OLD 15380  ordtypelem7OLD 15381  omsublimOLD 15396  infenomsubOLD 15398  omsubinitOLD 15399  ntruni 15412  clsint2 15414  opnnei 15417  cptclsscpt 15432  uncomp 15433  hscptsscld 15434  compfipin0lem 15435  compfipin0 15436  alexsublem1 15437  alexsublem2 15438  alexsublem3 15439  alexsub 15441  reconnlem3 15448  reconnlem5 15450  2ndc1stc 15477  2ndcctbss 15478  fneint 15486  reftr 15497  topfneec 15501  fnessref 15503  refssfne 15504  finptfin 15507  finlocfin 15509  lfinpfin 15513  locfincomp 15514  locfindsc 15515  comppfsc 15517  neibastop1 15518  neibastop2lem2 15520  neibastop2lem3 15521  neibastop2lem4 15522  topmtcl 15525  topmeet 15526  topjoin 15527  fnemeet1 15528  fnemeet2 15529  fnejoin1 15530  fnejoin2 15531  neifg 15559  supfil 15560  filssufillem 15570  uffixfr 15575  fixufil 15576  ufinffr 15578  cnpfillim 15589  rnelfm 15593  fmfnfm 15598  fmufil 15599  sfcls 15604  flimfcls 15613  fcluscnplem 15617  fcluscomplem 15620  fcluscomp 15621  tailmap 15636  tailuni 15638  ralunOLD 15657  fimax 15746  frinfm 15758  fisup2g 15768  sdclem2 15810  sdc 15811  fdc 15812  seqpo 15814  cnimass 15888  cnresima 15891  sstotbnd 15936  ismtyhmeolem 15950  heiborlem16 15970  heiborlem19 15973  rrnmet 16016  rrntotbnd 16022  iccbnd 16026  phtpyco 16056  isringd 16097  0idl 16173  intidl 16177  unichnidl 16179  prnc 16215  erreft 16259  0nelqs2 16269  hgrablkne0 16295  hgrablkcard 16296  smoge 16454  addrcom 16475  paddcl 17303

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-ral 2109

Copyright terms: Public domain