HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem keepel 2389
Description: Keep a membership hypothesis for weak deduction theorem, when special case B e. C is provable.
Hypotheses
Ref Expression
keepel.1 |- A e. C
keepel.2 |- B e. C
Assertion
Ref Expression
keepel |- if(ph, A, B) e. C
Proof of Theorem keepel
StepHypRef Expression
1 eleq1 1526 . 2 |- (A = if(ph, A, B) -> (A e. C <-> if(ph, A, B) e. C))
2 eleq1 1526 . 2 |- (B = if(ph, A, B) -> (B e. C <-> if(ph, A, B) e. C))
3 keepel.1 . 2 |- A e. C
4 keepel.2 . 2 |- B e. C
51, 2, 3, 4keephyp 2386 1 |- if(ph, A, B) e. C
Colors of variables: wff set class
Syntax hints:   e. wcel 955  ifcif 2351
This theorem is referenced by:  ifex 2390  divmulz 5675  divclz 5680  divcan1z 5687  divcan2z 5688  recne0z 5694  divrecz 5701  divdirz 5712  divcan3z 5716  rec11 5734  redivclz 5755  prodgt0 5775  ltmul1 5778  ltdiv1 5780  ltrec 5827  discrlem2 6587  sqrlem21 6623  sqrlem22 6624  sqrth 6629  sqrcl 6630  sqrgt0 6631  sqrmul 6635  abslem2 6846  dscmet 7856  projlem7 9108  omls 9161  osumlem8 9502
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452
This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-if 2352
Copyright terms: Public domain