Theorem rcla4ev 1924

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 1012	. 2 ⊢ (ψ → ∀xψ)
2		rcla4v.1	. 2 ⊢ (x = A → (φ ↔ ψ))
3	1, 2	rcla4e 1919	1 ⊢ ((A ∈ B ⋀ ψ) → ∃x ∈ B φ)

Syntax hints:   → wi 3   ↔ wb 153   ⋀ wa 230   = wceq 997   ∈ wcel 999  ∃wrex 1693

This theorem is referenced by:  rcla4edv 1926  rcla42ev 1928  wefrc 3000  onfr 3043  ordunidif 3062  onssmin 3065  onuninsuci 3165  tfrlem12 3980  oawordeulem 4246  oaass 4253  oarec 4254  odi 4268  omass 4269  oen0 4271  oeordi 4272  oelim2 4280  nneob 4313  snfi 4493  fiprlemOLD 4494  mapenlem2 4555  onfin 4584  pssnn 4599  ssnnfi 4600  unfi 4614  pwfilem 4630  supmaxlem 4648  suppr 4650  supsnALT 4652  trcl 4707  r1ord 4717  tz9.12lem3 4723  tz9.12 4724  scottex 4778  scott0 4779  aceq6b 4804  numth2 4847  oncardval 4881  cardaleph 4950  cardalephex 4951  alephfplem4 4964  alephfp2 4966  cflem 4970  cflecard 4977  cfsuc 4980  cnegex 5413  1re 5500  recex 5749  posexi 5968  nn2ge 6002  nndiv 6020  nominpos 6104  lbinfm 6130  infm3lem 6135  infmrcl 6151  xrsupsslem 6158  xrinfmsslem 6159  supxrpnf 6170  zdiv 6270  z2ge 6273  uzwo4OLD 6295  btwnz 6300  zq 6312  qbtwnre 6331  qbtwnxr 6332  flval3 6351  iccsupr 6424  icoshftf1oii 6435  uzwo 6481  uzwoOLD 6482  uzinfmi 6488  fsequb 6549  expnbnd 6743  sqrlem6 6768  abs1mi 6994  seq1bndi 7000  cau5ii 7007  cvg1 7011  cvg3i 7013  cvganz 7014  caubndi 7016  clm3i 7169  clm4i 7170  climconsti 7184  climshfti 7194  climrecl 7200  climge0 7202  climaddlem3 7206  climmullem8 7217  climubii 7243  caucvglem2 7248  caucvglem5 7251  caucvglem6 7252  caucvg2i 7255  caucvg3lem 7256  caucvg3 7258  serzf0i 7259  ser1f0i 7260  ser1clim0 7263  cvgcmp2lem 7270  cvgcmpubi 7275  infcvgaux2i 7310  expcnvlem1 7317  expcnvlem6 7322  elcncf1di 7360  efaddlem25 7452  efcn 7514  reeff1olem1 7515  reeff1o 7517  infpnlem2 7599  ruclem33 7634  infxpidmlem11 7654  topbas 7716  subtop 7733  retopbas 7740  clsval 7762  elcls 7789  neiint 7804  neips 7812  opnneissb 7813  opnssneib 7814  innei 7821  islp2 7832  blex 7934  blss 7938  blssex 7939  ssblex 7941  opnm 7945  blssopn 7952  opnin 7954  neibl 7962  blnei 7964  metcnp 7972  metcnpi3 7977  metcnpi4 7978  metcni2 7980  tgioolem 7999  lmconst 8019  lmnn 8020  lmuni 8036  metcnp4 8055  xplm 8060  xpcn 8061  iscms2lem4 8077  bcthlem2 8085  bcthlem7 8090  isgrp 8126  isgrpi 8127  grpinvf 8163  grplactf1o 8182  ghgrpilem3 8219  cnring 8246  ringsn 8247  nmcnilem 8421  va1cnlem 8429  sm1cnilem 8431  nmosetn0 8512  nmolb 8518  nmobndi 8522  nmo0 8535  nmlno0lem 8537  isblo3i 8545  blo3i 8546  blocnilem 8548  blocni 8549  ubthlem14 8626  minveclem10 8638  minveclem39 8671  htthlem7 8710  spwpr4OLD 8746  spwpr4aOLD 8747  pilem2 8755  pilem3 8756  efifolem1 8805  efifolem2 8806  efifolem6 8810  effoi 8828  hlim0 9188  norm1exi 9205  projlem8 9276  projlem10 9278  shsel3 9362  ococin 9380  spanval 9382  spancl 9387  shsumval2i 9443  h1de2ctlem 9561  spansncol 9574  pjoml6i 9615  nmopsetn0 9875  nmfnsetn0 9888  nmoplb 9914  nmfnlb 9931  adjvalval 9944  0cnop 9986  0cnfn 9987  idcnop 9988  nmop0 9993  nmfn0 9994  nmlnop0iALT 10003  nmopun 10022  nmcopexlem6 10039  lnopconi 10046  lnopcnbd 10048  nmcfnexlem6 10068  lnfnconi 10073  lnfncnbd 10075  riesz3i 10078  riesz1 10081  cnlnadjlem2 10084  cnlnadjlem8 10090  cnlnadjlem9 10091  adjbd1o 10101  branmfn 10121  pjnmopi 10158  pjhmopidm 10193  strlem1 10261  stri 10268  hstri 10276  cvcon3 10295  cvnbtwn 10297  superpos 10365  shatomici 10369  atcvat4i 10408  mdsymlem2 10415  cdj1i 10444  cdj3lem2 10446  cdj3i 10452  cayleythlem 10498  rcla4devOLD 10518  abfi 10534  ficli 10553  hmeogrp 10632  homcard 10633  fgsb 10663  efilcp 10664  fgsb2 10668  efilcp2 10669  iintlem1 10714  iintlem2 10715  trran 10718  idfisf 10844

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-12 1009  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-an 232  df-ex 1022  df-sb 1214  df-clab 1510  df-cleq 1515  df-clel 1518  df-rex 1697  df-v 1859

Copyright terms: Public domain