Theorem keepel 2395

Description: Keep a membership hypothesis for weak deduction theorem, when special case B ∈ C is provable.

Hypotheses

Ref	Expression
keepel.1	⊢ A ∈ C
keepel.2	⊢ B ∈ C

Assertion

Ref	Expression
keepel	⊢ if(φ, A, B) ∈ C

Proof of Theorem keepel

Step	Hyp	Ref	Expression
1		eleq1 1531	. 2 ⊢ (A = if(φ, A, B) → (A ∈ C ↔ if(φ, A, B) ∈ C))
2		eleq1 1531	. 2 ⊢ (B = if(φ, A, B) → (B ∈ C ↔ if(φ, A, B) ∈ C))
3		keepel.1	. 2 ⊢ A ∈ C
4		keepel.2	. 2 ⊢ B ∈ C
5	1, 2, 3, 4	keephyp 2392	1 ⊢ if(φ, A, B) ∈ C

Syntax hints:   ∈ wcel 956   ifcif 2357

This theorem is referenced by:  ifex 2396  divmulz 5683  divclz 5688  divcan1z 5695  divcan2z 5696  recne0z 5702  divrecz 5709  divdirz 5720  divcan3z 5724  rec11 5742  redivclz 5763  prodgt0 5783  ltmul1 5786  ltdiv1 5788  ltrec 5835  discrlem2 6595  sqrlem21 6631  sqrlem22 6632  sqrth 6637  sqrcl 6638  sqrgt0 6639  sqrmul 6643  abslem2 6854  dscmet 7870  projlem7 9131  omls 9184  osumlem8 9525

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-if 2358

Copyright terms: Public domain