Theorem rcla4ev 2381

Description: Restricted existential specialization, using implicit substitition.

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

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  E.wrex 2106

This theorem is referenced by:  rcla4edv 2383  rcla42ev 2385  wefrc 3652  onfr 3702  ordunidif 3712  onssmin 3878  onuninsuci 3921  dffv2 4734  tfrlem12 5130  oawordeulem 5236  oaass 5243  oarec 5244  odi 5258  omass 5259  oen0 5261  oeordi 5262  oelim2 5270  nneob 5312  ecelqsi 5350  snfi 5491  riota5 5580  mapenlem2 5584  onfin 5613  pssnn 5628  ssnnfi 5629  unfi 5644  pwfilem 5660  supmaxlem 5678  suppr 5680  supsnALT 5682  onsdom 5694  trcl 5752  r1ord 5766  tz9.12lem3 5772  tz9.12 5773  scottex 5846  scott0 5847  oncardval 5865  omsublim 5887  infenomsub 5889  omsubinit 5890  aceq6b 5904  numth2 5947  cardaleph 6033  cardalephex 6034  alephfplem4 6047  alephfp2 6049  cflem 6053  cflecard 6060  cfsuc 6063  cnegex 6502  1re 6598  recex 6876  posexi 7091  nn2ge 7125  nndiv 7143  nominpos 7230  lbinfm 7257  infm3lem 7262  infmrcl 7278  xrsupsslem 7285  xrinfmsslem 7286  supxrpnf 7297  zdiv 7397  z2ge 7400  uzwo4OLD 7422  btwnz 7428  zq 7440  qbtwnre 7459  qbtwnxr 7460  flval3 7479  iccsupr 7567  icoshftf1oii 7578  uzwo 7624  uzwoOLD 7625  uzinfmi 7631  fsequb 7702  expnbnd 7901  sqrlem6 7928  abs1mi 8156  seq1bndi 8162  cau5ii 8169  cvg1 8173  cvg3i 8175  cvganz 8176  caubndi 8178  clm3i 8339  clm4i 8340  climconsti 8354  climshfti 8364  climrecl 8370  climge0 8372  climaddlem3 8376  climmullem8 8387  climubii 8413  caucvglem2 8418  caucvglem5 8421  caucvglem6 8422  caucvg2i 8425  caucvg3lem 8426  caucvg3 8428  serzf0i 8429  ser1clim0 8433  cvgcmp2lem 8440  cvgcmpubi 8446  infcvgaux2i 8481  expcnvlem1 8488  expcnvlem6 8493  elcncf1di 8532  efaddlem25 8624  efcn 8688  reeff1olem1 8689  reeff1o 8691  infpnlem2 8776  ruclem33 8811  infxpidmlem11 8831  fiinbas 8885  topbas 8897  subbas 8914  subtop 8916  retopbas 8925  clsval 8953  elcls 8980  neiint 8995  neips 9003  opnneissb 9004  opnssneib 9005  innei 9012  islp2 9023  blex 9126  blss 9130  blssex 9131  ssblex 9133  opnm 9137  blssopn 9144  opnin 9146  neibl 9154  blnei 9156  metcnp 9165  metcnpi3 9170  metcnpi4 9171  metcni2 9173  tgioolem 9192  lmconst 9212  lmnn 9213  lmuni 9229  metcnp4 9248  xplm 9253  xpcn 9254  iscms2lem4 9270  bcthlem2 9278  bcthlem7 9283  isgrp 9321  isgrpi 9322  grpinvf 9364  grplactf1o 9406  ghgrpilem3 9443  cnring 9489  ringsn 9490  vacnlem3 9669  nmcnilem 9676  va1cnlem 9684  sm1cnilem 9686  nmosetn0 9767  nmolb 9773  nmobndi 9777  nmo0 9791  nmlno0lem 9793  isblo3i 9801  blo3i 9802  blocnilem 9804  blocni 9805  ubthlem14 9887  minveclem10 9899  minveclem39 9932  htthlem7 9973  spwpr4 10006  spwpr4OLD 10007  spwpr4aOLD 10008  pilem2 10021  pilem3 10022  efifolem1 10076  efifolem2 10077  efifolem6 10081  effoi 10099  axgroth6 10137  dif1en 10172  indexfi 10174  ficard 10176  findcard 10178  abfi 10215  fiuni 10219  elsubsp 10248  subspid 10249  subcld 10254  subtopmetlem 10255  filfbas 10276  fsubbas 10281  fbssfg 10285  fbfgss 10288  fgfil 10290  extbas1 10291  filrn 10293  hausfillim 10303  elfilmap 10312  elfilmap2 10313  elfilmap3 10314  cncomp 10331  fintopcomp 10333  lpni 10347  tosdir 10358  opidon 10369  rngmgmbs4 10401  hlim0 10738  norm1exi 10755  projlem8 10826  projlem10 10828  shsel3 10912  ococin 10930  spanval 10932  spancl 10937  shsumval2i 10993  h1de2ctlem 11111  spansncol 11124  pjoml6i 11165  nmopsetn0 11429  nmfnsetn0 11442  nmoplb 11468  nmfnlb 11485  adjvalval 11498  0cnop 11540  0cnfn 11541  idcnop 11542  nmop0 11547  nmfn0 11548  nmlnop0iALT 11557  nmopun 11576  nmcopexlem6 11593  lnopconi 11600  lnopcnbd 11602  nmcfnexlem6 11622  lnfnconi 11627  lnfncnbd 11629  riesz3i 11632  riesz1 11635  cnlnadjlem2 11638  cnlnadjlem8 11644  cnlnadjlem9 11645  adjbd1o 11655  branmfn 11675  branmfnOLD 11676  opsqrlem1 11711  pjnmopi 11719  pjhmopidm 11754  strlem1 11822  stri 11829  hstri 11837  cvcon3 11856  cvnbtwn 11858  superpos 11926  shatomici 11930  atcvat4i 11969  mdsymlem2 11976  cdj1i 12005  cdj3lem2 12007  cdj3i 12013  cayleythlem 13645  ublbneg 13653  lbzbi 13657  dvds0lem 13665  dvds1lem 13666  dvds2lem 13667  divalglem9 13704  gcdcllem3 13720  4nprm 13781  dfon2lem9 13857  tz6.26 13913  frmin 13938  poseq 13954  noxpsgn 13990  sltval2 13997  noreson 14001  elno2 14005  axbday 14012  axdenselem3 14021  axdenselem6 14024  axdense 14027  axfelem1 14031  axfelem3 14033  axfelem5 14035  axfelem7 14037  axfelem8 14038  axfelem9 14039  axfelem10 14040  axfelem12 14042  axfelem15 14045  ficli 14353  prj1 14395  surjsec 14462  npincppr 14501  repcpwti 14503  prl 14512  nZdef 14527  domncnt 14624  ranncnt 14625  rngsubpos 14636  latdir 14643  mgmlion 14697  symgfo 14730  trran2 14757  svs2 14829  unint2t 14866  intfmu2 14867  sallnei 14873  nsn 14874  osneisi 14875  hmeogrp 14892  homcard 14893  subspemp 14903  istopx 14918  fgsb 14921  efilcp 14922  fgsb2 14925  efilcp2 14926  conttnf 14944  altretoplem2 14996  altretop 14997  iintlem1 15010  iintlem2 15011  trran 15014  lvsovso 15038  idfisf 15189  idsubfun 15206  taralt 15211  partarelt1 15273  partarelt2 15274  fictblem 15370  finsschain 15373  onsdomOLD 15385  omsublimOLD 15396  infenomsubOLD 15398  omsubinitOLD 15399  opncldf1 15402  opnregcld 15415  cldregopn 15416  subsubtop 15423  subcls 15424  compsublem 15430  compsub 15431  cptclsscpt 15432  uncomp 15433  hscptsscld 15434  compfipin0lem 15435  compfipin0 15436  alexsublem3 15439  alexsublem4 15440  alexsub 15441  reconnlem4 15449  2ndcsb 15476  2ndc1stc 15477  2ndcctbss 15478  fness 15491  ssref 15492  fneref 15493  refref 15494  fnessref 15503  refssfne 15504  finlocfin 15509  locfindsc 15515  comppfsc 15517  neibastop1 15518  neibastop2lem3 15521  neibastop2lem4 15522  neibastop2 15523  fnemeet1 15528  fnemeet2 15529  fnejoin1 15530  ist1-2 15542  ist1-3 15543  isnrm2 15552  opnfbas 15557  filfinnfr 15561  ufileu 15573  uffixfr 15575  flimcls 15588  cnpfillim 15589  imaelfm 15591  rnelfmlem 15592  rnelfm 15593  fmfnfmlem1 15594  fmfnfmlem3 15596  fmfnfmlem4 15597  fmfnfm 15598  filfm 15600  flimfbas 15601  isfclus 15606  fcluscf 15612  fclsfnflim 15614  flimfnfcls 15615  fcluscnplem 15617  fcluscomplem 15620  fcluscomp 15621  tailfb 15639  filnetlem3 15642  filnetlem5 15644  filnet 15645  unirep 15664  cover2 15673  foco2 15686  f1elima 15719  fimax 15746  fisupg 15748  indexa 15753  indexfiOLD 15755  frinfm 15758  fisup2g 15768  frfi 15771  sdc 15811  fdc 15812  incsequz 15815  subspopn 15837  subspcld 15838  subspabs 15840  geomcau 15849  caushft 15851  metdcn 15853  icoopnst 15876  iocopnst 15877  cnres 15889  cnss 15892  tlmconst 15907  txsubsp 15912  txmet 15925  sstotbnd 15936  totbndss 15937  isbnd3 15941  blbnd 15943  totbndbnd 15944  ismtyhmeolem 15950  heiborlem1 15955  heiborlem16 15970  heiborlem18 15972  heiborlem21 15975  heiborlem23 15977  heiborlem35 15989  heiborlem38 15992  heiborlem42 15996  bfp 16009  recms 16010  rrntotbnd 16022  iccbnd 16026  exidres 16031  isgrpda 16033  isgrpd 16034  isabld 16036  elpi1i 16090  pi1gp 16095  isringd 16097  isdivrng2 16111  igenval 16209  igenidl 16211  prnc 16215  fnelstr 16717  strdif 16719  cvrcon3b 16994  glbcon 17028  cvrat4 17076  ps2 17079  isgrpiNEW 17115  atompoint 17224  elpaddn0 17261  ispsubcl2 17356

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-rex 2110  df-v 2294

Copyright terms: Public domain