Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifeq1 Structured version   Unicode version

Theorem ifeq1 3744
 Description: Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
Assertion
Ref Expression
ifeq1

Proof of Theorem ifeq1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 rabeq 2951 . . 3
21uneq1d 3501 . 2
3 dfif6 3743 . 2
4 dfif6 3743 . 2
52, 3, 43eqtr4g 2494 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wceq 1653  crab 2710   cun 3319  cif 3740 This theorem is referenced by:  ifeq12  3753  ifeq1d  3754  ifbieq12i  3761  ifexg  3799  rdgeq2  6671  dfoi  7481  wemaplem2  7517  cantnflem1  7646  sumeq2w  12487  sumeq2ii  12488  mplcoe3  16530  ellimc  19761  ply1nzb  20046  dchrvmasumiflem1  21196  prodeq2w  25239  prodeq2ii  25240  dfrdg2  25424  dfafv2  27973 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-rab 2715  df-v 2959  df-un 3326  df-if 3741
 Copyright terms: Public domain W3C validator