Theorem rexbidv 2124

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

Hypothesis

Ref	Expression
ralbidv.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
rexbidv	|- (ph -> (E.x e. A ps <-> E.x e. A ch))

Distinct variable group:   ph,x

Proof of Theorem rexbidv

Step	Hyp	Ref	Expression
1		ax-17 1317	. 2 |- (ph -> A.xph)
2		ralbidv.1	. 2 |- (ph -> (ps <-> ch))
3	1, 2	rexbid 2122	1 |- (ph -> (E.x e. A ps <-> E.x e. A ch))

Syntax hints:   -> wi 3   <-> wb 163  E.wrex 2106

This theorem is referenced by:  2rexbidv 2141  rexralbidv 2142  rexeqbi1dv 2272  rexeqbidv 2275  rcla42ev 2385  ceqsrex2v 2395  sbcrexg 2533  uniiunlem 2693  eliun 3259  dfiun2gOLD 3284  dfiin2g 3286  dfiin2OLD 3288  iunrab 3299  iununi 3331  iununiOLD 3332  eufromeq2 3829  eufromeq6 3833  euobj1 3834  orduninsuc 3925  elimag 4269  funcnvuni 4482  fvelrnb 4719  fvelimaOLD 4724  fvelimab 4725  abrexexlem2 4835  funiunfv 4842  abrexex2 4847  f1oiso 4881  f1oweALT 4883  elrnoprabg 5066  onopriun 5118  tfrlem3 5121  tfrlem12 5130  rdgeq1 5142  rdgeq2 5143  nneob 5312  qseq2 5347  elqs 5348  elqsi 5349  isfi 5441  enfi 5627  pssnn 5628  unblem1 5633  unblem2 5634  unbnn2 5638  supmo 5666  suplub 5671  ordtype 5691  tz9.13 5774  omsublim 5887  aceq1 5891  aceq2 5893  aceq5lem3 5899  aceq5lem4 5900  aceq6a 5903  aceq6b 5904  kmlem9 5935  kmlem12 5938  kmlem14 5940  numth2 5947  numthcor 5948  zorn2lem7 5956  brdom3 5963  brdom7disj 5966  brdom6disj 5967  cardiun 6011  cflim 6057  prnmax 6251  genpv 6254  axrnegex 6436  axrrecex 6437  cnegex 6502  recex 6876  infm3 7263  infmsup 7277  nnunb 7279  arch 7280  xrsupsslem 7285  xrinfmsslem 7286  xrsupss 7287  xrinfmss 7288  xrub 7289  supxrre 7292  supxrunb1 7298  supxrunb2 7299  qbtwnxr 7460  fsequb 7702  limsupval 7772  creur 7992  creui 7993  reval 8005  imval 8006  replim 8011  cau3iri 8167  sumeq1 8242  dffsum 8258  clm0i 8343  clm0nnsi 8345  clm4a 8350  climabs0i 8373  caucvg3 8428  dfisum 8452  infcvgaux2i 8481  infcvglem1 8482  expcnv 8494  cncfval 8526  negfcncfi 8531  reeff1olem2 8690  unbenlem 8773  basis2 8884  eltg2 8889  tg2 8891  tgval3 8895  tgss2 8907  basgen2 8909  subtop 8916  txval 8932  txbas 8933  neival 8993  isnei 8994  isneip 8996  cnpval 9035  iscnp 9036  cnpimaex 9041  isopn 9136  opni 9141  opnin 9146  metcnp 9165  metcnp2 9166  metcnpi 9168  metcnpi2 9169  metcni 9172  metcnss 9176  cncfmet 9183  tgioo 9193  lmbrf 9208  cmscvg 9225  lmss 9231  iscms2lem5 9271  cncms 9276  bcth 9310  isgrp 9321  isgrpi 9322  grpidinvlem3 9330  grpideu 9333  grpidinv2 9344  isgrp2i 9360  ghgrpilem3 9443  ringid 9469  nvcni 9661  nvcni2 9662  nvcni3 9663  va1cnlem 9684  sm1cnilem 9686  nvcnpi3 9761  nvcnpi4 9762  nmofval 9764  nmoval 9765  nmosetn0 9767  nmolb 9773  nmoubi 9774  nmlno0lem 9793  minveclem9 9898  minveclem10 9899  minveclem14 9903  minveclem24 9913  minvecex 9923  spwpr4 10006  spwpr4OLD 10007  spwpr4aOLD 10008  efghgrpilem 10073  efifolem3 10078  circgrp 10094  grothomex 10136  indexfi 10174  subsp 10244  issubsp 10245  issubsplem1 10246  fbasssin 10278  fbssint 10279  fbfgss 10288  filrn 10293  hausfillim 10303  isfilmap 10308  filmapss 10309  elfilmap 10312  flimfneii 10320  iscomp 10330  cncomp 10331  dirge 10357  h2hcau 10481  h2hlm 10482  hcau 10684  hhcms 10705  chcompl 10748  hhsscms 10783  projlem8 10826  projlem10 10828  projlem13 10831  projlem15 10833  projlem17 10835  projlem29 10847  pjtheui 10868  pjval 10872  pjeq2 10874  pjpj0i 10888  shsumval 10910  h1de2ci 11112  elspansn 11122  osumlem5 11217  nmopval 11419  elcnop 11420  nmopsetn0 11429  nmfnval 11440  nmfnsetn0 11442  elcnfn 11446  eigvecval 11459  nmoplb 11468  nmopub 11469  cnopc 11474  nmfnlb 11485  nmfnleub 11486  cnfnc 11491  eleigvec 11518  nmlnop0iALT 11557  nmopun 11576  nmcopexlem1 11588  lnopcon 11601  nmcfnexlem1 11617  lnfncon 11628  branmfn 11675  branmfnOLD 11676  pjnmopi 11719  cvbr 11854  hatomic 11932  chrelat2 11942  cdjreui 12004  cdj3lem2 12007  bnj1366 13091  bnj64 13201  bnj873 13317  bnj1234 13460  bnj1314 13492  bnj1313 13494  cayleythlem 13645  divides 13664  divalglem4 13699  divalglem10 13705  divalg 13706  gcdcllem3 13720  orderseqlem 13953  poseq 13954  soseq 13955  elno 13987  sltval 13988  axfelem5 14035  axfelem8 14038  axfelem9 14039  axfelem15 14045  axfelem16 14046  altxpeq2 14097  iscst1 14519  iscst2 14520  iscst4 14522  prodeq1 14658  prodeq3 14663  dffprod 14670  sallnei 14873  hmeogrp 14892  subsp2 14902  subspemp 14903  fgsb 14921  fgsb2 14925  cnfilca 14927  fbaslim2 14936  iscnp3 14946  altretop 14997  cntrset 15000  isfuna 15182  isfunb 15183  settrcon 15247  vtarsuelt 15272  partarelt2 15274  dfiin2gOLD 15356  fictblem 15370  fictb 15371  finsschain 15373  ordtypeOLD 15382  omsublimOLD 15396  compsublem 15430  compsub 15431  hscptsscld 15434  compfipin0lem 15435  alexsub 15441  1stcclb 15471  is2ndc 15472  2ndc1stc 15477  2ndcctbss 15478  isfne3 15482  fnessex 15484  refssex 15490  fnessref 15503  islocfin 15506  comppfsc 15517  neibastop1 15518  neibastop2lem2 15520  neibastop2lem3 15521  neibastop2lem4 15522  neibastop2 15523  neibastop3 15524  fnemeet1 15528  fnemeet2 15529  fnejoin2 15531  t0dist 15541  ist1-2 15542  ist1-3 15543  t1sep 15546  nrmsep2 15555  ufinffr 15578  ufilen 15579  cnpfillim 15589  rnelfmlem 15592  rnelfm 15593  fmfnfmlem3 15596  fmfnfmlem4 15597  fmfnfm 15598  fcluscf 15612  flimfnfcls 15615  fcluscnplem 15617  fcluscomplem 15620  fcluscomp 15621  ufcomp 15622  tailfb 15639  filnetlem2 15641  unirep 15664  foelrn 15685  foco2 15686  eropreu 15733  abrexex2g 15738  indexa 15753  indexfiOLD 15755  sdclem2 15810  sdc 15811  fdc 15812  fdc1 15813  incsequz 15815  lmclim2 15850  txmet 15925  istotbnd 15933  sstotbnd 15936  totbndss 15937  isbnd 15939  isbnd3 15941  bndss 15942  blbnd 15943  totbndbnd 15944  ismtyhmeolem 15950  ismtybndlem 15952  heiborlem1 15955  heiborlem10 15964  heiborlem16 15970  heiborlem18 15972  heiborlem20 15974  heiborlem23 15977  heiborlem34 15988  heiborlem35 15989  heiborlem40 15994  heiborlem42 15996  isgrpda 16033  pi1bval 16088  elpi1 16089  isdivrng2 16111  divrngidl 16176  prnc 16215  isfldidl 16216  elqs2 16267  prter3 16286  elstr 16714  stb2strx 16747  stb3strx 16754  cvrval 16988  atlatex 17013  glbconx 17029  hlsuprexch 17033  isgrpNEW 17104  grpidinvlem3NEW 17111  grpideuNEW 17114  isgrpiNEW 17115  grpidinv2NEW 17119  plusssval 17205  ispoint 17223  pmapglbx 17251  paddval 17259  elpaddn0 17261  elpaddat 17265  elpadd0 17270

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-rex 2110

Copyright terms: Public domain