Theorem exbidv 1274

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

Hypothesis

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

Assertion

Ref	Expression
exbidv	|- (ph -> (E.xps <-> E.xch))

Distinct variable group:   ph,x

Proof of Theorem exbidv

Step	Hyp	Ref	Expression
1		ax-17 968	. 2 |- (ph -> A.xph)
2		albidv.1	. 2 |- (ph -> (ps <-> ch))
3	1, 2	exbid 1101	1 |- (ph -> (E.xps <-> E.xch))

Syntax hints:   -> wi 3   <-> wb 146  E.wex 977

This theorem is referenced by:  2exbidv 1276  3exbidv 1277  sb7f 1336  eubid 1378  eleq1 1526  eleq2 1527  rexbidv2 1658  ceqsex2 1827  eqvinc 1874  alexeq 1876  ceqex 1877  sbc5g 1944  sbcexg 1965  sbcabel 1986  sbcel12g 2001  eluni 2496  unieq 2500  intab 2550  cbvopab1 2664  cbvopab1s 2665  csbopabg 2668  axrep1 2684  axrep2 2685  axrep3 2686  zfrepclf 2689  axsep2 2694  zfauscl 2695  opabid 2799  uniuni 2870  coeq1 3270  coeq2 3271  opelco 3277  opelcog 3279  dfdmf 3295  eldm 3296  eldm2g 3298  dmsnop 3317  dfrnf 3334  elrn2 3335  iss 3381  cores 3485  ndmfv 3730  fnrnfv 3744  ssimaexg 3754  dmfco 3758  fvco 3759  funiunfv 3851  rdglem2 3923  rdglim2 3934  cbvoprab12 3983  2ndconst 4081  elqsi 4275  mapsn 4329  breng 4357  brdomg 4358  domeng 4362  abfii3 4537  abfii4 4538  fodomfi 4540  zfregcl 4567  inf0 4578  axinf 4595  bnd2 4696  aceq0 4702  aceq3lem 4704  aceq3 4705  aceq5lem4 4710  aceq5 4712  axac 4717  ac7g 4721  ac4c 4723  ac5 4724  kmlem1 4737  kmlem2 4738  kmlem8 4744  kmlem10 4746  kmlem13 4749  cfval 4878  cardcf 4883  cfeq0 4886  cfsuc 4887  axrepndlem1 4916  axunndlem1 4919  zfcndrep 4938  zfcndinf 4942  zfcndac 4943  ltexpi 5001  recmulpq 5042  ltexpq 5052  ltexpq2 5053  halfpq 5054  genpn0 5078  genpnmax 5082  1idpr 5105  ltexprlem3 5116  ltexprlem4 5117  ltexpri 5121  reclem2pr 5129  recexpr 5132  recexsrlem 5184  map2psrpr 5192  suppsr 5194  supsrlem6 5202  supre 5232  infm3 6001  infmsup 6015  nnunb 6017  sumeq1 6920  sumeq2 6923  dffsum 6936  cvgcmp3cetlem1 7124  isumclim3t 7135  isumclim5t 7137  efseq1ex 7248  eftlext 7320  acdc3 7429  acdc5 7435  infxpidmlem2 7496  eltg3t 7568  subbas 7586  subbas2 7587  ismet 7737  isgrp 7975  spwval2 8577  cayleythlem 10320  spfi 10346  fiv 10374  hmph 10411  hmeogrp 10425  efilcp 10445  fisub 10447

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978

Copyright terms: Public domain