Theorem rexbidv 1710

Description: Formula-building rule for restricted existential quantifier (deduction rule).

Hypothesis

Ref	Expression
ralbidv.1	⊢ (φ → (ψ ↔ χ))

Assertion

Ref	Expression
rexbidv	⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ))

Distinct variable group:   φ,x

Proof of Theorem rexbidv

Step	Hyp	Ref	Expression
1		ax-17 1007	. 2 ⊢ (φ → ∀xφ)
2		ralbidv.1	. 2 ⊢ (φ → (ψ ↔ χ))
3	1, 2	rexbid 1708	1 ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ))

Syntax hints:   → wi 3   ↔ wb 144  ∃wrex 1692

This theorem is referenced by:  2rexbidv 1727  rexralbidv 1728  rexeqd 1838  rexeq12d 1841  rcla42ev 1927  ceqsrex2v 1936  uniiunlem 2184  eliun 2637  dfiun2g 2654  dfiin2 2656  iunrab 2664  iununi 2686  orduninsuc 3197  elimag 3499  funcnvuni 3669  fvelrnb 3871  fvelima 3875  abrexexlem2 3973  funiunfv 3980  abrexex2 3985  f1oiso 4018  f1oweALT 4020  elrnoprabg 4186  onopriun 4211  tfrlem3 4214  tfrlem12 4223  rdgeq1 4235  rdgeq2 4236  nneob 4395  qseq2 4429  elqs 4430  elqsi 4431  isfi 4523  enfi 4680  pssnn 4681  unblem1 4686  unblem2 4687  unbnn2 4691  supmo 4719  suplub 4724  tz9.13 4809  aceq1 4875  aceq2 4877  aceq5lem3 4883  aceq5lem4 4884  aceq6a 4887  aceq6b 4888  kmlem9 4919  kmlem12 4922  kmlem14 4924  numth2 4931  numthcor 4932  zorn2lem7 4940  brdom3 4947  brdom7disj 4950  brdom6disj 4951  cardiun 5009  cflim 5059  prnmax 5253  genpv 5256  axrnegex 5437  axrrecex 5438  cnegex 5502  recex 5840  infm3 6222  infmsup 6236  nnunb 6238  arch 6239  xrsupsslem 6244  xrinfmsslem 6245  xrsupss 6246  xrinfmss 6247  xrub 6248  supxrre 6251  supxrunb1 6257  supxrunb2 6258  qbtwnxr 6419  fsequb 6654  limsupval 6724  creur 6943  creui 6944  reval 6956  imval 6957  replim 6962  cau3iri 7118  sumeq1 7185  dffsum 7201  clm0i 7286  clm0nnsi 7288  clm4a 7293  climabs0i 7316  caucvg3 7371  dfisum 7395  infcvgaux2i 7424  infcvglem1 7425  expcnv 7437  cncfval 7469  negfcncfi 7474  reeff1olem2 7633  unbenlem 7716  basis2 7827  eltg2 7831  tg2 7833  tgval3 7837  tgss2 7849  basgen2 7851  subtop 7858  neival 7927  isnei 7928  isneip 7930  cnpval 7969  iscnp 7970  cnpimaex 7975  isopn 8069  opni 8074  opnin 8079  metcnp 8098  metcnp2 8099  metcnpi 8101  metcnpi2 8102  metcni 8105  metcnss 8109  cncfmet 8116  tgioo 8126  lmbrf 8141  cmscvg 8158  lmss 8164  iscms2lem5 8204  cncms 8209  bcth 8243  isgrp 8254  isgrpi 8255  grpidinvlem3 8263  grpideu 8266  grpidinv2 8277  isgrp2i 8293  ghgrpilem3 8376  ringid 8386  nvcni 8576  nvcni2 8577  nvcni3 8578  va1cnlem 8599  sm1cnilem 8601  nvcnpi3 8676  nvcnpi4 8677  nmofval 8679  nmoval 8680  nmosetn0 8682  nmolb 8688  nmoubi 8689  nmlno0lem 8708  minveclem9 8813  minveclem10 8814  minveclem14 8818  minveclem24 8828  minvecex 8838  spwpr4 8925  spwpr4OLD 8926  spwpr4aOLD 8927  efghgrpilem 8991  efifolem3 8996  circgrp 9012  grothinf 9053  h2hcau 9124  h2hlm 9125  hcau 9327  hhcms 9348  chcompl 9391  hhsscms 9426  projlem8 9469  projlem10 9471  projlem13 9474  projlem15 9476  projlem17 9478  projlem29 9490  pjtheui 9511  pjval 9515  pjeq2 9517  pjpj0i 9531  shsumval 9553  h1de2ci 9755  elspansn 9765  osumlem5 9860  nmopval 10062  elcnop 10063  nmopsetn0 10072  nmfnval 10083  nmfnsetn0 10085  elcnfn 10089  eigvecval 10102  nmoplb 10111  nmopub 10112  cnopc 10117  nmfnlb 10128  nmfnleub 10129  cnfnc 10134  eleigvec 10161  nmlnop0iALT 10199  nmopun 10218  nmcopexlem1 10230  lnopcon 10243  nmcfnexlem1 10259  lnfncon 10270  branmfn 10317  branmfnOLD 10318  pjnmopi 10355  cvbr 10490  hatomic 10568  chrelat2 10578  cdjreui 10641  cdj3lem2 10644  cayleythlem 10698  sallnei 11016  hmeogrp 11044  subsp 11056  issubsp 11057  issubsplem1 11058  subspemp 11060  fgsb 11082  fgsb2 11086  cnfilca 11088  iscomp 11114  altretop 11144  isfuna 11288  isfunb 11289  dfiin2g 11400  fictblem 11422  fictb 11423  finsschain 11425  ordtype 11434  omsublim 11448  compsublem 11487  compsub 11488  hscptsscld 11491  compfipin0lem 11492  cncomp 11494  alexsub 11500  1stcclb 11532  is2ndc 11533  2ndc1stc 11538  2ndcctbss 11539  isfne3 11543  fnessex 11545  refssex 11551  fnessref 11564  islocfin 11567  comppfsc 11578  neibastop1 11579  neibastop2lem2 11581  neibastop2lem3 11582  neibastop2lem4 11583  neibastop2 11584  neibastop3 11585  fnemeet1 11589  fnemeet2 11590  fnejoin2 11592  t0dist 11602  ist1-2 11603  ist1-3 11604  t1sep 11607  nrmsep2 11616  fbasssin 11625  fbssint 11626  fbfgss 11640  filrn 11643  ufinffr 11663  ufilen 11664  hausfillim 11685  cnpfillim 11686  isfilmap 11689  elfilmap 11690  filmapss 11696  rnelfmlem 11698  rnelfm 11699  fmfnfmlem3 11702  fmfnfmlem4 11703  fmfnfm 11704  flimfneii 11712  fcluscf 11724  flimfnfcls 11727  fcluscnplem 11729  fcluscomplem 11732  fcluscomp 11733  ufcomp 11734  dirge 11754  tailfb 11762  filnetlem2 11764  abrexex2g 11825  indexa 11845  indexf 11847  sdclem2 11876  sdc 11877  incsequz 11879  metsstop 11909  lmclim2 11915  txval 11972  txbas 11973  istotbnd 11989  sstotbnd 11992  totbndss 11993  isbnd 11995  isbnd3 11997  bndss 11998  blbnd 11999  totbndbnd 12000  ismtyhmeolem 12006  ismtybndlem 12008  heiborlem1 12011  heiborlem10 12020  heiborlem16 12026  heiborlem18 12028  heiborlem20 12030  heiborlem23 12033  heiborlem34 12044  heiborlem35 12045  heiborlem40 12050  heiborlem42 12052

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-rex 1696

Copyright terms: Public domain