Theorem treq 5199

Description: Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.)

Assertion

Ref	Expression
treq	⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))

Proof of Theorem treq

Step	Hyp	Ref	Expression
1		unieq 4861	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
2	1	sseq1d 3953	. . 3 ⊢ (𝐴 = 𝐵 → (∪ 𝐴 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐴))
3		sseq2 3948	. . 3 ⊢ (𝐴 = 𝐵 → (∪ 𝐵 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐵))
4	2, 3	bitrd 279	. 2 ⊢ (𝐴 = 𝐵 → (∪ 𝐴 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐵))
5		df-tr 5193	. 2 ⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)
6		df-tr 5193	. 2 ⊢ (Tr 𝐵 ↔ ∪ 𝐵 ⊆ 𝐵)
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ⊆ wss 3889  ∪ cuni 4850  Tr wtr 5192

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-uni 4851  df-tr 5193

This theorem is referenced by:  truni  5208  trint  5210  ordeq  6330  trcl  9649  tz9.1  9650  tz9.1c  9651  tctr  9659  tcmin  9660  tc2  9661  r1tr  9700  r1elssi  9729  tcrank  9808  iswun  10627  tskr1om2  10691  elgrug  10715  grutsk  10745  tz9.1regs  35278  dfon2lem1  35963  dfon2lem3  35965  dfon2lem4  35966  dfon2lem5  35967  dfon2lem6  35968  dfon2lem7  35969  dfon2lem8  35970  dfon2  35972  tz9.1tco  36665  dfttc3gw  36705  dford3lem1  43454  dford3lem2  43455  nadd1rabtr  43816  wfaxext  45420  wfaxrep  45421  wfaxpow  45424  wfaxinf2  45428  wfac8prim  45429