Theorem tceq 6159

Description: Equality theorem for cardinal T operator. (Contributed by SF, 2-Mar-2015.)

Assertion

Ref	Expression
tceq	|- (A = B -> Tc A = Tc B)

Proof of Theorem tceq

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rexeq 2809	. . . 4 |- (A = B -> (E.y e. A x = Nc ~P1 y <-> E.y e. B x = Nc ~P1 y))
2	1	anbi2d 684	. . 3 |- (A = B -> ((x e. NC /\ E.y e. A x = Nc ~P1 y) <-> (x e. NC /\ E.y e. B x = Nc ~P1 y)))
3	2	iotabidv 4361	. 2 |- (A = B -> (iotax(x e. NC /\ E.y e. A x = Nc ~P1 y)) = (iotax(x e. NC /\ E.y e. B x = Nc ~P1 y)))
4		df-tc 6104	. 2 |- Tc A = (iotax(x e. NC /\ E.y e. A x = Nc ~P1 y))
5		df-tc 6104	. 2 |- Tc B = (iotax(x e. NC /\ E.y e. B x = Nc ~P1 y))
6	3, 4, 5	3eqtr4g 2410	1 |- (A = B -> Tc A = Tc B)

Syntax hints:   -> wi 4   /\ wa 358   = wceq 1642   e. wcel 1710  E.wrex 2616  ~P₁ cpw1 4136  iotacio 4338   NC cncs 6089   Nc cnc 6092   T_c ctc 6094

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-rex 2621  df-uni 3893  df-iota 4340  df-tc 6104

This theorem is referenced by:  tcdi  6165  tc2c  6167  tc11  6229  taddc  6230  tlecg  6231  letc  6232  ce0t  6233  ce2le  6234  cet  6235  tce2  6237  te0c  6238  ce0lenc1  6240  tlenc1c  6241  brtcfn  6247  nmembers1lem1  6269  nmembers1  6272  nchoicelem1  6290  nchoicelem2  6291  nchoicelem12  6301  nchoicelem16  6305  nchoicelem17  6306  nchoicelem19  6308  nchoice  6309