Theorem ifeq1 3945

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.

Step	Hyp	Ref	Expression
1		rabeq 3103	. . 3
2	1	uneq1d 3656	. 2
3		dfif6 3944	. 2
4		dfif6 3944	. 2
5	2, 3, 4	3eqtr4g 2523	1

Syntax hints:  -.wn 3  ->wi 4  =wceq 1395  {crab 2811  u.cun 3473  ifcif 3941

This theorem is referenced by:  ifeq12  3958  ifeq1d  3959  ifbieq12i  3967  ifexg  4011  rdgeq2  7097  dfoi  7957  wemaplem2  7993  cantnflem1  8129  cantnflem1OLD  8152  prodeq2w  13719  prodeq2ii  13720  mgm2nsgrplem2  16037  mgm2nsgrplem3  16038  mplcoe3  18128  mplcoe3OLD  18129  marrepval0  19063  ellimc  22277  ply1nzb  22523  dchrvmasumiflem1  23686  signspval  28509  dfrdg2  29228  dfafv2  32217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-un 3480  df-if 3942