Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  trsbc Unicode version

Theorem trsbc 28304
Description: Formula-building inference rule for class substitution, substituting a class variable for the set variable of the transitivity predicate. trsbc 28304 is trsbcVD 28653 without virtual deductions and was automatically derived from trsbcVD 28653 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
trsbc  |-  ( A  e.  V  ->  ( [. A  /  x ]. Tr  x  <->  Tr  A
) )
Distinct variable group:    x, A
Allowed substitution hint:    V( x)

Proof of Theorem trsbc
Dummy variables  y 
z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dftr2 4115 . . 3  |-  ( Tr  x  <->  A. z A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
21sbcbiiOLD 3047 . 2  |-  ( A  e.  V  ->  ( [. A  /  x ]. Tr  x  <->  [. A  /  x ]. A. z A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) ) )
3 sbcalg 3039 . . . 4  |-  ( A  e.  V  ->  ( [. A  /  x ]. A. z A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. z [. A  /  x ]. A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) ) )
4 sbcalg 3039 . . . . . 6  |-  ( A  e.  V  ->  ( [. A  /  x ]. A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) ) )
5 pm3.31 432 . . . . . . . . . 10  |-  ( ( z  e.  y  -> 
( y  e.  x  ->  z  e.  x ) )  ->  ( (
z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
6 pm3.3 431 . . . . . . . . . 10  |-  ( ( ( z  e.  y  /\  y  e.  x
)  ->  z  e.  x )  ->  (
z  e.  y  -> 
( y  e.  x  ->  z  e.  x ) ) )
75, 6impbii 180 . . . . . . . . 9  |-  ( ( z  e.  y  -> 
( y  e.  x  ->  z  e.  x ) )  <->  ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
87sbcbiiOLD 3047 . . . . . . . 8  |-  ( A  e.  V  ->  ( [. A  /  x ]. ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) ) )
9 sbcim2g 28302 . . . . . . . . . 10  |-  ( A  e.  V  ->  ( [. A  /  x ]. ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( [. A  /  x ]. z  e.  y  ->  ( [. A  /  x ]. y  e.  x  ->  [. A  /  x ]. z  e.  x ) ) ) )
10 biidd 228 . . . . . . . . . . . 12  |-  ( x  =  A  ->  (
z  e.  y  <->  z  e.  y ) )
1110sbcieg 3023 . . . . . . . . . . 11  |-  ( A  e.  V  ->  ( [. A  /  x ]. z  e.  y  <->  z  e.  y ) )
12 sbcel2gv 3051 . . . . . . . . . . 11  |-  ( A  e.  V  ->  ( [. A  /  x ]. y  e.  x  <->  y  e.  A ) )
13 sbcel2gv 3051 . . . . . . . . . . 11  |-  ( A  e.  V  ->  ( [. A  /  x ]. z  e.  x  <->  z  e.  A ) )
14 imbi13 28283 . . . . . . . . . . 11  |-  ( (
[. A  /  x ]. z  e.  y  <->  z  e.  y )  -> 
( ( [. A  /  x ]. y  e.  x  <->  y  e.  A
)  ->  ( ( [. A  /  x ]. z  e.  x  <->  z  e.  A )  -> 
( ( [. A  /  x ]. z  e.  y  ->  ( [. A  /  x ]. y  e.  x  ->  [. A  /  x ]. z  e.  x ) )  <->  ( z  e.  y  ->  ( y  e.  A  ->  z  e.  A ) ) ) ) ) )
1511, 12, 13, 14syl3c 57 . . . . . . . . . 10  |-  ( A  e.  V  ->  (
( [. A  /  x ]. z  e.  y  ->  ( [. A  /  x ]. y  e.  x  ->  [. A  /  x ]. z  e.  x
) )  <->  ( z  e.  y  ->  ( y  e.  A  ->  z  e.  A ) ) ) )
169, 15bitrd 244 . . . . . . . . 9  |-  ( A  e.  V  ->  ( [. A  /  x ]. ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( z  e.  y  ->  ( y  e.  A  ->  z  e.  A ) ) ) )
17 pm3.31 432 . . . . . . . . . 10  |-  ( ( z  e.  y  -> 
( y  e.  A  ->  z  e.  A ) )  ->  ( (
z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
18 pm3.3 431 . . . . . . . . . 10  |-  ( ( ( z  e.  y  /\  y  e.  A
)  ->  z  e.  A )  ->  (
z  e.  y  -> 
( y  e.  A  ->  z  e.  A ) ) )
1917, 18impbii 180 . . . . . . . . 9  |-  ( ( z  e.  y  -> 
( y  e.  A  ->  z  e.  A ) )  <->  ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
2016, 19syl6bb 252 . . . . . . . 8  |-  ( A  e.  V  ->  ( [. A  /  x ]. ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( (
z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) )
218, 20bitr3d 246 . . . . . . 7  |-  ( A  e.  V  ->  ( [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  ( (
z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) )
2221albidv 1611 . . . . . 6  |-  ( A  e.  V  ->  ( A. y [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y
( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) )
234, 22bitrd 244 . . . . 5  |-  ( A  e.  V  ->  ( [. A  /  x ]. A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) )
2423albidv 1611 . . . 4  |-  ( A  e.  V  ->  ( A. z [. A  /  x ]. A. y ( ( z  e.  y  /\  y  e.  x
)  ->  z  e.  x )  <->  A. z A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) )
253, 24bitrd 244 . . 3  |-  ( A  e.  V  ->  ( [. A  /  x ]. A. z A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. z A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) )
26 dftr2 4115 . . 3  |-  ( Tr  A  <->  A. z A. y
( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
2725, 26syl6bbr 254 . 2  |-  ( A  e.  V  ->  ( [. A  /  x ]. A. z A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  Tr  A
) )
282, 27bitrd 244 1  |-  ( A  e.  V  ->  ( [. A  /  x ]. Tr  x  <->  Tr  A
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1527    = wceq 1623    e. wcel 1684   [.wsbc 2991   Tr wtr 4113
This theorem is referenced by:  truniALT  28305  truniALTVD  28654  trintALTVD  28656  trintALT  28657
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-sbc 2992  df-in 3159  df-ss 3166  df-uni 3828  df-tr 4114
  Copyright terms: Public domain W3C validator