Theorem rcla4ev 1923

Description: Restricted existential specialization, using implicit substitition.

Hypothesis

Ref	Expression
rcla4v.1	⊢ (x = A → (φ ↔ ψ))

Assertion

Ref	Expression
rcla4ev	⊢ ((A ∈ B ⋀ ψ) → ∃x ∈ B φ)

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

Proof of Theorem rcla4ev

Step	Hyp	Ref	Expression
1		ax-17 1007	. 2 ⊢ (ψ → ∀xψ)
2		rcla4v.1	. 2 ⊢ (x = A → (φ ↔ ψ))
3	1, 2	rcla4e 1918	1 ⊢ ((A ∈ B ⋀ ψ) → ∃x ∈ B φ)

Syntax hints:   → wi 3   ↔ wb 144   ⋀ wa 221   = wceq 992   ∈ wcel 994  ∃wrex 1692

This theorem is referenced by:  rcla4edv 1925  rcla42ev 1927  wefrc 2970  onfr 3014  ordunidif 3022  onssmin 3154  onuninsuci 3194  tfrlem12 4223  oawordeulem 4324  oaass 4331  oarec 4332  odi 4346  omass 4347  oen0 4349  oeordi 4350  oelim2 4358  nneob 4395  ecelqsi 4432  snfi 4573  mapenlem2 4637  onfin 4666  pssnn 4681  ssnnfi 4682  unfi 4697  pwfilem 4713  supmaxlem 4731  suppr 4733  supsnALT 4735  trcl 4791  r1ord 4801  tz9.12lem3 4807  tz9.12 4808  scottex 4862  scott0 4863  aceq6b 4888  numth2 4931  oncardval 4965  cardaleph 5035  cardalephex 5036  alephfplem4 5049  alephfp2 5051  cflem 5055  cflecard 5062  cfsuc 5065  cnegex 5502  1re 5589  recex 5840  posexi 6053  nn2ge 6087  nndiv 6105  nominpos 6189  lbinfm 6216  infm3lem 6221  infmrcl 6237  xrsupsslem 6244  xrinfmsslem 6245  supxrpnf 6256  zdiv 6356  z2ge 6359  uzwo4OLD 6381  btwnz 6387  zq 6399  qbtwnre 6418  qbtwnxr 6419  flval3 6438  iccsupr 6525  icoshftf1oii 6536  uzwo 6582  uzwoOLD 6583  uzinfmi 6589  fsequb 6654  expnbnd 6852  sqrlem6 6879  abs1mi 7107  seq1bndi 7113  cau5ii 7120  cvg1 7124  cvg3i 7126  cvganz 7127  caubndi 7129  clm3i 7282  clm4i 7283  climconsti 7297  climshfti 7307  climrecl 7313  climge0 7315  climaddlem3 7319  climmullem8 7330  climubii 7356  caucvglem2 7361  caucvglem5 7364  caucvglem6 7365  caucvg2i 7368  caucvg3lem 7369  caucvg3 7371  serzf0i 7372  ser1clim0 7376  cvgcmp2lem 7383  cvgcmpubi 7389  infcvgaux2i 7424  expcnvlem1 7431  expcnvlem6 7436  elcncf1di 7475  efaddlem25 7567  efcn 7631  reeff1olem1 7632  reeff1o 7634  infpnlem2 7719  ruclem33 7754  infxpidmlem11 7774  topbas 7839  subbas 7856  subtop 7858  retopbas 7865  clsval 7887  elcls 7914  neiint 7929  neips 7937  opnneissb 7938  opnssneib 7939  innei 7946  islp2 7957  blex 8059  blss 8063  blssex 8064  ssblex 8066  opnm 8070  blssopn 8077  opnin 8079  neibl 8087  blnei 8089  metcnp 8098  metcnpi3 8103  metcnpi4 8104  metcni2 8106  tgioolem 8125  lmconst 8145  lmnn 8146  lmuni 8162  metcnp4 8181  xplm 8186  xpcn 8187  iscms2lem4 8203  bcthlem2 8211  bcthlem7 8216  isgrp 8254  isgrpi 8255  grpinvf 8297  grplactf1o 8339  ghgrpilem3 8376  cnring 8404  ringsn 8405  vacnlem3 8584  nmcnilem 8591  va1cnlem 8599  sm1cnilem 8601  nmosetn0 8682  nmolb 8688  nmobndi 8692  nmo0 8706  nmlno0lem 8708  isblo3i 8716  blo3i 8717  blocnilem 8719  blocni 8720  ubthlem14 8802  minveclem10 8814  minveclem39 8847  htthlem7 8888  spwpr4 8925  spwpr4OLD 8926  spwpr4aOLD 8927  pilem2 8939  pilem3 8940  efifolem1 8994  efifolem2 8995  efifolem6 8999  effoi 9017  hlim0 9381  norm1exi 9398  projlem8 9469  projlem10 9471  shsel3 9555  ococin 9573  spanval 9575  spancl 9580  shsumval2i 9636  h1de2ctlem 9754  spansncol 9767  pjoml6i 9808  nmopsetn0 10072  nmfnsetn0 10085  nmoplb 10111  nmfnlb 10128  adjvalval 10141  0cnop 10182  0cnfn 10183  idcnop 10184  nmop0 10189  nmfn0 10190  nmlnop0iALT 10199  nmopun 10218  nmcopexlem6 10235  lnopconi 10242  lnopcnbd 10244  nmcfnexlem6 10264  lnfnconi 10269  lnfncnbd 10271  riesz3i 10274  riesz1 10277  cnlnadjlem2 10280  cnlnadjlem8 10286  cnlnadjlem9 10287  adjbd1o 10297  branmfn 10317  branmfnOLD 10318  pjnmopi 10355  pjhmopidm 10390  strlem1 10458  stri 10465  hstri 10473  cvcon3 10492  cvnbtwn 10494  superpos 10562  shatomici 10566  atcvat4i 10606  mdsymlem2 10613  cdj1i 10642  cdj3lem2 10644  cdj3i 10650  cayleythlem 10698  abfi 10737  ficli 10756  prj1 10809  domncnt 10872  ranncnt 10873  opidon 10898  rngmgmbs4 10945  sallnei 11016  nsn 11017  osneisi 11018  hmeogrp 11044  homcard 11045  subspemp 11060  fgsb 11082  efilcp 11083  fgsb2 11086  efilcp2 11087  fintopcomp 11115  altretoplem2 11143  altretop 11144  iintlem1 11155  iintlem2 11156  trran 11159  idfisf 11295  idsubfun 11312  lpni 11417  fiuni 11420  fictblem 11422  finsschain 11425  onsdom 11437  omsublim 11448  infenomsub 11450  omsubinit 11451  opncldf1 11454  opnregcld 11467  cldregopn 11468  elsubsp 11477  subspid 11478  subsubtop 11479  subcld 11480  subcls 11481  compsublem 11487  compsub 11488  cptclsscpt 11489  uncomp 11490  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  cncomp 11494  alexsublem3 11498  alexsublem4 11499  alexsub 11500  subtopmetlem 11505  reconnlem4 11510  2ndcsb 11537  2ndc1stc 11538  2ndcctbss 11539  fness 11552  ssref 11553  fneref 11554  refref 11555  fnessref 11564  refssfne 11565  finlocfin 11570  locfindsc 11576  comppfsc 11578  neibastop1 11579  neibastop2lem3 11582  neibastop2lem4 11583  neibastop2 11584  fnemeet1 11589  fnemeet2 11590  fnejoin1 11591  ist1-2 11603  ist1-3 11604  isnrm2 11613  filfbas 11628  opnfbas 11629  fsubbas 11630  fbssfg 11635  fgfil 11638  fbfgss 11640  extbas1 11641  filrn 11643  filfinnfr 11646  ufileu 11658  uffixfr 11660  flimcls 11684  hausfillim 11685  cnpfillim 11686  elfilmap 11690  elfilmap2 11691  elfilmap3 11692  imaelfm 11695  rnelfmlem 11698  rnelfm 11699  fmfnfmlem1 11700  fmfnfmlem3 11702  fmfnfmlem4 11703  fmfnfm 11704  filfm 11706  flimfbas 11713  isfclus 11718  fcluscf 11724  fclsfnflim 11726  flimfnfcls 11727  fcluscnplem 11729  fcluscomplem 11732  fcluscomp 11733  tosdir 11755  tailfb 11762  filnetlem3 11765  filnetlem5 11767  filnet 11768  f1elima 11818  ficard 11834  fimax 11837  fisupg 11839  indexa 11845  indexf 11847  frinfm 11850  sdc 11877  incsequz 11879  subspopn 11900  subspcld 11901  subspabs 11903  fiinbas 11905  geomcau 11914  caushft 11916  metdcn 11918  icoopnst 11940  iocopnst 11941  cnres 11950  cnss 11953  tlmconst 11968  txsubsp 11983  sstotbnd 11992  totbndss 11993  isbnd3 11997  blbnd 11999  totbndbnd 12000  ismtyhmeolem 12006  heiborlem1 12011  heiborlem16 12026  heiborlem18 12028  heiborlem21 12031  heiborlem23 12033  heiborlem35 12045  heiborlem38 12048  heiborlem42 12052  bfp 12065  recms 12066  rrntotbnd 12078  iccbnd 12082

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-rex 1696  df-v 1858

Copyright terms: Public domain