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

Theorem ifeq1 3793
Description: Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
Assertion
Ref Expression
ifeq1  |-  ( A  =  B  ->  if ( ph ,  A ,  C )  =  if ( ph ,  B ,  C ) )

Proof of Theorem ifeq1
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 rabeq 2964 . . 3  |-  ( A  =  B  ->  { x  e.  A  |  ph }  =  { x  e.  B  |  ph } )
21uneq1d 3507 . 2  |-  ( A  =  B  ->  ( { x  e.  A  |  ph }  u.  {
x  e.  C  |  -.  ph } )  =  ( { x  e.  B  |  ph }  u.  { x  e.  C  |  -.  ph } ) )
3 dfif6 3792 . 2  |-  if (
ph ,  A ,  C )  =  ( { x  e.  A  |  ph }  u.  {
x  e.  C  |  -.  ph } )
4 dfif6 3792 . 2  |-  if (
ph ,  B ,  C )  =  ( { x  e.  B  |  ph }  u.  {
x  e.  C  |  -.  ph } )
52, 3, 43eqtr4g 2498 1  |-  ( A  =  B  ->  if ( ph ,  A ,  C )  =  if ( ph ,  B ,  C ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1369   {crab 2717    u. cun 3324   ifcif 3789
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rab 2722  df-v 2972  df-un 3331  df-if 3790
This theorem is referenced by:  ifeq12  3804  ifeq1d  3805  ifbieq12i  3813  ifexg  3857  rdgeq2  6866  dfoi  7723  wemaplem2  7759  cantnflem1  7895  cantnflem1OLD  7918  sumeq2w  13167  mplcoe3  17543  mplcoe3OLD  17544  marrepval0  18370  ellimc  21346  ply1nzb  21592  dchrvmasumiflem1  22748  signspval  26951  prodeq2w  27423  prodeq2ii  27424  dfrdg2  27607  dfafv2  30035  scmatid  30879  scmatsubcl  30881  scmatmulcl  30883
  Copyright terms: Public domain W3C validator