Theorem rcla4ev 1877

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 971	. 2 |- (ps -> A.xps)
2		rcla4v.1	. 2 |- (x = A -> (ph <-> ps))
3	1, 2	rcla4e 1872	1 |- ((A e. B /\ ps) -> E.x e. B ph)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 956   e. wcel 958  E.wrex 1646

This theorem is referenced by:  rcla4edv 1879  rcla42ev 1881  wefrc 2943  onfr 2986  ordunidif 3005  onssmin 3008  onuninsuc 3108  tfrlem12 3922  oawordeulem 4188  oaass 4195  oarec 4196  odi 4210  omass 4211  oen0 4213  oeordi 4214  oelim2 4222  nneob 4255  snfi 4432  snfiOLD 4433  mapenlem2 4490  onfinOLD 4520  pssnn 4534  ssnnfi 4535  ssnnfiOLD 4536  unfi 4551  unfiOLD 4552  unifiOLD 4557  pwfilemOLD 4570  pwfiOLD 4571  supmaxlem 4588  suppr 4590  supsnALT 4592  trcl 4645  r1ord 4655  tz9.12lem3 4661  tz9.12 4662  scottex 4716  scott0 4717  aceq6b 4742  numth2 4785  oncardval 4819  cardaleph 4885  cardalephex 4886  alephfplem4 4899  alephfp2 4901  cflem 4905  cflecard 4912  cfsuc 4915  cnegext 5348  1re 5435  recext 5684  posex 5908  nn2get 5942  nndivt 5959  nominpos 6043  lbinfm 6048  infm3lem 6053  infmrcl 6069  xrsupsslem 6076  xrinfmsslem 6077  supxrpnf 6088  z2get 6188  uzwo4OLD 6210  btwnz 6215  flval3t 6239  zqt 6260  qbtwnre 6278  qbtwnxr 6279  iccsupr 6398  icoshftf1oi 6409  uzwo 6455  uzwoOLD 6456  uzinfm 6462  fsequb 6523  expnbndt 6654  sqrlem6 6678  abs1m 6904  seq1bnd 6910  cau5i 6917  cvg1 6921  cvg3 6923  cvganz 6924  caubnd 6926  clm3 7079  clm4 7080  climconst 7094  climshft 7104  climrecl 7110  climge0 7112  climaddlem3 7116  climmullem8 7127  climubi 7153  caucvglem2 7158  caucvglem5 7161  caucvglem6 7162  caucvg2 7165  caucvg3lem 7166  caucvg3t 7168  serzf0 7169  ser1f0 7170  ser1clim0 7173  cvgcmp2lem 7180  cvgcmpub 7185  infcvgaux2 7220  expcnvlem1 7227  expcnvlem6 7232  elcncf1d 7270  efaddlem25 7362  efcn 7423  reeff1olem1 7424  reeff1o 7426  infpnlem2 7507  ruclem33 7542  infxpidmlem11 7562  topbast 7627  subbasOLD 7644  subtop 7646  retopbas 7655  clsval 7677  elcls 7704  neiint 7719  neips 7727  opnneissb 7728  opnssneib 7729  innei 7736  islp2 7747  blex 7849  blss 7853  blssex 7854  ssblex 7856  opnm 7860  blssopn 7867  opnin 7869  neibl 7877  blnei 7879  metcnp 7887  metcnpi3 7892  metcnpi4 7893  metcni2 7895  tgioolem 7914  lmconst 7934  lmnn 7935  lmuni 7951  metcnp4 7970  xplm 7975  xpcn 7976  iscms2lem4 7992  bcthlem2 8000  bcthlem7 8005  isgrp 8041  isgrpi 8042  grpinvf 8079  grplactf1o 8098  ghgrpilem3 8135  cnring 8162  ringsn 8163  nmcnilem 8337  va1cnlem 8345  sm1cnilem 8347  nmosetn0 8428  nmolb 8434  nmobndi 8438  nmo0 8451  nmlno0lem 8453  isblo3i 8461  blo3i 8462  blocnilem 8464  blocni 8465  ubthlem14 8542  minveclem10 8554  minveclem39 8587  htthlem7 8626  spwpr4OLD 8663  spwpr4aOLD 8664  pilem2 8672  pilem3 8673  efifolem1 8722  efifolem2 8723  efifolem6 8727  effoi 8745  hlim0 9105  norm1ex 9122  projlem8 9193  projlem10 9195  shsel3t 9279  ococint 9297  spanvalt 9299  spanclt 9304  shsumval2 9360  h1de2ctlem 9478  spansncol 9491  pjoml6 9532  nmopsetn0 9792  nmfnsetn0 9805  nmoplbt 9831  nmfnlbt 9848  adjvalvalt 9861  0cnop 9903  0cnfn 9904  idcnop 9905  nmop0 9910  nmfn0 9911  nmlnop0ALT 9920  nmopunt 9939  nmcopexlem6 9956  lnopcon 9963  lnopcnbdt 9965  nmcfnexlem6 9985  lnfncon 9990  lnfncnbdt 9992  riesz3 9995  riesz1t 9998  cnlnadjlem2 10001  cnlnadjlem8 10007  cnlnadjlem9 10008  adjbd1o 10018  branmfnt 10038  pjnmop 10075  pjhmopidm 10110  strlem1 10177  str 10184  hstr 10192  cvcon3t 10211  cvnbtwnt 10213  superpos 10281  shatomic 10285  atcvat4 10324  mdsymlem2 10331  cdj1 10360  cdj3lem2 10362  cdj3 10368  cayleythlem 10413  rcla4devOLD 10431  abfi 10451  abfiOLD 10452  ficli 10472  ficliOLD 10473  hmeogrp 10538  homcard 10539  set2elt 10545  setwoe 10546  fgsb 10570  fgsbOLD 10571  efilcp 10572  efilcpOLD 10573  fgsb2 10580  efilcp2 10581  efilcp2OLD 10582  iintlem1 10632  iintlem2 10633  trran 10636  idfisf 10760

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-rex 1650  df-v 1812

Copyright terms: Public domain