Mathbox for Jonathan Ben-Naim < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj882 Unicode version

Theorem bnj882 29274
 Description: Definition (using hypotheses for readability) of the function giving the transitive closure of in by . (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
bnj882.1
bnj882.2
bnj882.3
bnj882.4
Assertion
Ref Expression
bnj882
Distinct variable groups:   ,,,,   ,,,,   ,,,,
Allowed substitution hints:   (,,,)   (,,,)   (,,,)   (,,,)

Proof of Theorem bnj882
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 df-bnj18 29036 . 2
2 df-iun 3923 . . 3
3 df-iun 3923 . . . 4
4 bnj882.4 . . . . . . . . 9
5 bnj882.1 . . . . . . . . . . . . . . 15
6 bnj882.2 . . . . . . . . . . . . . . 15
75, 6anbi12i 678 . . . . . . . . . . . . . 14
87anbi2i 675 . . . . . . . . . . . . 13
9 3anass 938 . . . . . . . . . . . . 13
10 3anass 938 . . . . . . . . . . . . 13
118, 9, 103bitr4i 268 . . . . . . . . . . . 12
1211rexbii 2581 . . . . . . . . . . 11
13 bnj882.3 . . . . . . . . . . . . . 14
1413eleq2i 2360 . . . . . . . . . . . . 13
1514anbi1i 676 . . . . . . . . . . . 12
1615rexbii2 2585 . . . . . . . . . . 11
1712, 16bitri 240 . . . . . . . . . 10
1817abbii 2408 . . . . . . . . 9
194, 18eqtri 2316 . . . . . . . 8
2019eleq2i 2360 . . . . . . 7
2120anbi1i 676 . . . . . 6
2221rexbii2 2585 . . . . 5
2322abbii 2408 . . . 4
243, 23eqtr4i 2319 . . 3
252, 24eqtr4i 2319 . 2
261, 25eqtr4i 2319 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   w3a 934   wceq 1632   wcel 1696  cab 2282  wral 2556  wrex 2557   cdif 3162  c0 3468  csn 3653  ciun 3921   csuc 4410  com 4672   cdm 4705   wfn 5266  cfv 5271   c-bnj14 29029   c-bnj18 29035 This theorem is referenced by:  bnj893  29276  bnj906  29278  bnj916  29281  bnj983  29299  bnj1014  29308  bnj1145  29339  bnj1318  29371 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277 This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-rex 2562  df-iun 3923  df-bnj18 29036
 Copyright terms: Public domain W3C validator