Theorem exbidv 1278

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

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

This theorem is referenced by:  2exbidv 1280  3exbidv 1281  sb7f 1340  eubid 1384  eleq1 1532  eleq2 1533  rexbidv2 1664  ceqsex2 1833  eqvinc 1880  alexeq 1882  ceqex 1883  sbc5g 1951  sbcexg 1972  sbcabel 1993  sbcel12g 2008  eluni 2502  unieq 2506  intab 2556  cbvopab1 2670  cbvopab1s 2671  csbopabg 2674  axrep1 2690  axrep2 2691  axrep3 2692  zfrepclf 2695  axsep2 2700  zfauscl 2701  opabid 2806  uniuni 2876  coeq1 3277  coeq2 3278  opelco 3284  opelcog 3286  dfdmf 3302  eldm 3303  eldm2g 3305  dmsnop 3324  dfrnf 3344  elrn2 3345  iss 3393  cores 3495  ndmfv 3740  fnrnfv 3754  ssimaexg 3764  dmfco 3768  fvco 3769  funiunfv 3861  rdglem2 3933  rdglim2 3944  cbvoprab12 3993  2ndconst 4090  elqsi 4284  mapsn 4338  breng 4366  brdomg 4367  domeng 4371  abfii3 4546  abfii4 4547  fodomfi 4549  zfregcl 4578  inf0 4589  axinf 4606  bnd2 4707  aceq0 4713  aceq3lem 4715  aceq3 4716  aceq5lem4 4721  aceq5 4723  axac 4728  ac7g 4732  ac4c 4734  ac5 4735  kmlem1 4748  kmlem2 4749  kmlem8 4755  kmlem10 4757  kmlem13 4760  cfval 4889  cardcf 4894  cfeq0 4897  cfsuc 4898  axrepndlem1 4927  axunndlem1 4930  zfcndrep 4949  zfcndinf 4953  zfcndac 4954  ltexpi 5012  recmulpq 5053  ltexpq 5063  ltexpq2 5064  halfpq 5065  genpn0 5089  genpnmax 5093  1idpr 5116  ltexprlem3 5127  ltexprlem4 5128  ltexpri 5132  reclem2pr 5140  recexpr 5143  recexsrlem 5195  map2psrpr 5203  suppsr 5205  supsrlem6 5213  supre 5243  infm3 6011  infmsup 6025  nnunb 6027  sumeq1 6935  sumeq2 6938  dffsum 6951  cvgcmp3cetlem1 7141  isumclim3t 7152  isumclim5t 7154  efseq1ex 7265  eftlext 7337  acdc3 7446  acdc5 7452  infxpidmlem2 7513  eltg3t 7586  subbas 7604  subbas2 7605  ismet 7758  isgrp 8003  spwval2 8610  cayleythlem 10369  spfi 10404  fiv 10433  hmph 10470  hmeogrp 10484  efilcp 10504  fisub 10506  rcfpfillem1 10511  rcfpfillem3 10513  rcfpfillem6 10516  rcfpfil 10517

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

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

Copyright terms: Public domain