Theorem exbidv 1277

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 969	. 2 |- (ph -> A.xph)
2		albidv.1	. 2 |- (ph -> (ps <-> ch))
3	1, 2	exbid 1103	1 |- (ph -> (E.xps <-> E.xch))

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

This theorem is referenced by:  2exbidv 1279  3exbidv 1280  sb7f 1339  eubid 1383  eleq1 1531  eleq2 1532  rexbidv2 1663  ceqsex2 1832  eqvinc 1879  alexeq 1881  ceqex 1882  sbc5g 1950  sbcexg 1971  sbcabel 1992  sbcel12g 2007  eluni 2501  unieq 2505  intab 2555  cbvopab1 2669  cbvopab1s 2670  csbopabg 2673  axrep1 2689  axrep2 2690  axrep3 2691  zfrepclf 2694  axsep2 2699  zfauscl 2700  opabid 2805  uniuni 2875  coeq1 3276  coeq2 3277  opelco 3283  opelcog 3285  dfdmf 3301  eldm 3302  eldm2g 3304  dmsnop 3323  dfrnf 3342  elrn2 3343  iss 3389  cores 3491  ndmfv 3736  fnrnfv 3750  ssimaexg 3760  dmfco 3764  fvco 3765  funiunfv 3857  rdglem2 3929  rdglim2 3940  cbvoprab12 3989  2ndconst 4087  elqsi 4281  mapsn 4335  breng 4363  brdomg 4364  domeng 4368  abfii3 4543  abfii4 4544  fodomfi 4546  zfregcl 4575  inf0 4586  axinf 4603  bnd2 4704  aceq0 4710  aceq3lem 4712  aceq3 4713  aceq5lem4 4718  aceq5 4720  axac 4725  ac7g 4729  ac4c 4731  ac5 4732  kmlem1 4745  kmlem2 4746  kmlem8 4752  kmlem10 4754  kmlem13 4757  cfval 4886  cardcf 4891  cfeq0 4894  cfsuc 4895  axrepndlem1 4924  axunndlem1 4927  zfcndrep 4946  zfcndinf 4950  zfcndac 4951  ltexpi 5009  recmulpq 5050  ltexpq 5060  ltexpq2 5061  halfpq 5062  genpn0 5086  genpnmax 5090  1idpr 5113  ltexprlem3 5124  ltexprlem4 5125  ltexpri 5129  reclem2pr 5137  recexpr 5140  recexsrlem 5192  map2psrpr 5200  suppsr 5202  supsrlem6 5210  supre 5240  infm3 6009  infmsup 6023  nnunb 6025  sumeq1 6928  sumeq2 6931  dffsum 6944  cvgcmp3cetlem1 7132  isumclim3t 7143  isumclim5t 7145  efseq1ex 7256  eftlext 7328  acdc3 7437  acdc5 7443  infxpidmlem2 7504  eltg3t 7576  subbas 7594  subbas2 7595  ismet 7748  isgrp 7991  spwval2 8595  cayleythlem 10347  spfi 10382  fiv 10410  hmph 10447  hmeogrp 10461  efilcp 10481  fisub 10483

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973

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

Copyright terms: Public domain