Theorem rcla4ev 1868

Description: Restricted existential specialization with implicit substitution.

Hypothesis

Ref	Expression
rcla4v.1	|- (x = A -> (ph <-> ps))

Assertion

Ref	Expression
rcla4ev	|- ((A e. B /\ ps) -> E.x e. B ph)

Distinct variable groups:   x,A   x,B   ps,x

Proof of Theorem rcla4ev

Step	Hyp	Ref	Expression
1		ax-17 968	. 2 |- (ps -> A.xps)
2		rcla4v.1	. 2 |- (x = A -> (ph <-> ps))
3	1, 2	rcla4e 1863	1 |- ((A e. B /\ ps) -> E.x e. B ph)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 953   e. wcel 955  E.wrex 1638

This theorem is referenced by:  rcla4edv 1870  rcla42ev 1872  wefrc 2933  onfr 2976  ordunidif 2995  onssmin 2998  onuninsuc 3098  tfrlem12 3907  oawordeulem 4172  oaass 4179  oarec 4180  odi 4194  omass 4195  oen0 4197  oeordi 4198  oelim2 4206  nneob 4239  snfi 4413  mapenlem2 4470  onfin 4499  pssnn 4513  ssnn 4514  unfi 4528  unifi 4532  pwfilem 4544  pwfi 4545  suppr 4562  supsnALT 4564  trcl 4617  r1ord 4627  tz9.12lem3 4633  tz9.12 4634  scottex 4688  scott0 4689  aceq6b 4714  numth2 4757  oncardval 4791  cardaleph 4857  cardalephex 4858  alephfplem4 4871  alephfp2 4873  cflem 4877  cflecard 4884  cfsuc 4887  cnegext 5320  1re 5407  recext 5657  posex 5856  nn2get 5890  nndivt 5906  nominpos 5990  lbinfm 5995  infm3lem 6000  infmrcl 6016  xrsupsslem 6023  xrinfmsslem 6024  supxrpnf 6035  z2get 6135  uzwo4OLD 6158  btwnz 6163  flval3t 6182  zqt 6198  qbtwnre 6216  qbtwnxr 6217  iccsupr 6331  icoshftf1oi 6342  uzwo 6387  uzwoOLD 6388  uzinfm 6394  fsequb 6455  expnbndt 6585  sqrlem6 6608  abs1m 6841  seq1bnd 6847  cau5i 6854  cvg1 6858  cvg3 6860  cvganz 6861  caubnd 6863  clm3 7017  clm4 7018  climconst 7031  climshft 7041  climrecl 7047  climge0 7049  climaddlem3 7052  climmullem8 7063  climubi 7089  caucvglem2 7094  caucvglem5 7097  caucvglem6 7098  caucvg2 7101  caucvg3lem 7102  caucvg3t 7104  serzf0 7105  ser1f0 7106  ser1clim0 7109  cvgcmp2lem 7116  cvgcmpub 7121  infcvgaux2 7155  expcnvlem1 7162  expcnvlem6 7167  elcncf1d 7205  ivthlem4OLD 7228  efaddlem25 7304  efcn 7363  reeff1olem1 7364  reeff1olem1OLD 7366  reeff1o 7368  infpnlem2 7450  ruclem33 7485  infxpidmlem11 7505  topbast 7569  subbas 7586  subtop 7588  retopbas 7597  clsval 7619  elcls 7646  neiint 7660  neips 7668  opnneissb 7669  opnssneib 7670  innei 7677  islp2 7688  blex 7789  blss 7793  blssex 7794  ssblex 7796  opnm 7800  blssopn 7807  opnin 7809  neibl 7817  blnei 7818  metcnp 7826  metcnpi3 7831  metcnpi4 7832  metcni2 7834  tgioolem 7853  lmconst 7872  lmnn 7873  lmuni 7886  metcnp4 7904  xplm 7909  xpcn 7910  iscms2lem4 7926  bcthlem2 7934  bcthlem7 7939  isgrp 7975  isgrpi 7976  grpinvf 8014  grplactf1o 8034  ghgrpilem3 8072  cnring 8099  ringsn 8100  nmcnilem 8272  va1cnlem 8279  sm1cnilem 8281  nmosetn0 8360  nmolb 8366  nmobndi 8370  nmo0 8383  nmlno0lem 8385  isblo3i 8392  blo3i 8393  blocnilem 8395  blocni 8396  ubthlem14 8473  minveclem10 8485  minveclem39 8518  htthlem7 8556  pilem2 8591  pilem3 8592  efifolem1 8637  efifolem2 8638  efifolem6 8642  effoi 8666  effoiOLD 8667  hlim0 9026  norm1ex 9043  projlem8 9109  projlem10 9111  shsel3t 9194  ococint 9212  spanvalt 9214  spanclt 9219  shsumval2 9275  h1de2ctlem 9394  spansncol 9407  pjoml6 9449  nmopsetn0 9709  nmfnsetn0 9722  nmoplbt 9748  nmfnlbt 9764  adjvalvalt 9777  0cnop 9819  0cnfn 9820  idcnop 9821  nmop0 9826  nmfn0 9827  nmlnop0ALT 9835  nmopunt 9854  nmcopexlem6 9871  lnopcon 9878  lnopcnbdt 9880  nmcfnexlem6 9900  lnfncon 9905  lnfncnbdt 9907  riesz3 9910  riesz1t 9913  cnlnadjlem2 9916  cnlnadjlem8 9922  cnlnadjlem9 9923  adjbd1o 9933  branmfnt 9951  pjnmop 9986  pjhmopidm 10020  strlem1 10087  str 10094  hstr 10102  cvcon3t 10121  cvnbtwnt 10123  superpos 10189  shatomic 10193  atcvat4 10232  mdsymlem2 10239  cdj1 10265  cdj3lem2 10267  cdj3 10273  cayleythlem 10320  rcla4devOLD 10331  abfi 10349  ficli 10368  hmeogrp 10425  homcard 10426  fgsb 10444  efilcp 10445  fgsb2 10449  efilcp2 10450  iintlem1 10476  iintlem2 10477  trran 10480

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-rex 1642  df-v 1803

Copyright terms: Public domain