Mathbox for Alan Sare < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  trintALT Structured version   Visualization version   Unicode version

Theorem trintALT 37278
 Description: The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. trintALT 37278 is an alternate proof of trint 4512. trintALT 37278 is trintALTVD 37277 without virtual deductions and was automatically derived from trintALTVD 37277 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
trintALT
Distinct variable group:   ,

Proof of Theorem trintALT
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 459 . . . . 5
21a1i 11 . . . 4
3 iidn3 36857 . . . . . . 7
4 id 22 . . . . . . . 8
5 rspsbc 3346 . . . . . . . 8
63, 4, 5ee31 37139 . . . . . . 7
7 trsbc 36901 . . . . . . . 8
87biimpd 211 . . . . . . 7
93, 6, 8ee33 36878 . . . . . 6
10 simpr 463 . . . . . . . . 9
1110a1i 11 . . . . . . . 8
12 elintg 4242 . . . . . . . . 9
1312ibi 245 . . . . . . . 8
1411, 13syl6 34 . . . . . . 7
15 rsp 2754 . . . . . . 7
1614, 15syl6 34 . . . . . 6
17 trel 4504 . . . . . . 7
1817expd 438 . . . . . 6
199, 2, 16, 18ee323 36864 . . . . 5
2019ralrimdv 2804 . . . 4
21 elintg 4242 . . . . 5
2221biimprd 227 . . . 4
232, 20, 22syl6c 66 . . 3
2423alrimivv 1774 . 2
25 dftr2 4499 . 2
2624, 25sylibr 216 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 371  wal 1442   wcel 1887  wral 2737  wsbc 3267  cint 4234   wtr 4497 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ral 2742  df-v 3047  df-sbc 3268  df-in 3411  df-ss 3418  df-uni 4199  df-int 4235  df-tr 4498 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator