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

Theorem trsbc 27961
Description: Formula-building inference rule for class substitution, substituting a class variable for the set variable of the transitivity predicate. trsbc 27961 is trsbcVD 28323 without virtual deductions and was automatically derived from trsbcVD 28323 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 4238 . . 3  |-  ( Tr  x  <->  A. z A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
21sbcbiiOLD 3153 . 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 3145 . . . 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 3145 . . . . . 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 433 . . . . . . . . . 10  |-  ( ( z  e.  y  -> 
( y  e.  x  ->  z  e.  x ) )  ->  ( (
z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
6 pm3.3 432 . . . . . . . . . 10  |-  ( ( ( z  e.  y  /\  y  e.  x
)  ->  z  e.  x )  ->  (
z  e.  y  -> 
( y  e.  x  ->  z  e.  x ) ) )
75, 6impbii 181 . . . . . . . . 9  |-  ( ( z  e.  y  -> 
( y  e.  x  ->  z  e.  x ) )  <->  ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
87sbcbiiOLD 3153 . . . . . . . 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 27959 . . . . . . . . . 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 229 . . . . . . . . . . . 12  |-  ( x  =  A  ->  (
z  e.  y  <->  z  e.  y ) )
1110sbcieg 3129 . . . . . . . . . . 11  |-  ( A  e.  V  ->  ( [. A  /  x ]. z  e.  y  <->  z  e.  y ) )
12 sbcel2gv 3157 . . . . . . . . . . 11  |-  ( A  e.  V  ->  ( [. A  /  x ]. y  e.  x  <->  y  e.  A ) )
13 sbcel2gv 3157 . . . . . . . . . . 11  |-  ( A  e.  V  ->  ( [. A  /  x ]. z  e.  x  <->  z  e.  A ) )
14 imbi13 27940 . . . . . . . . . . 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 59 . . . . . . . . . 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 245 . . . . . . . . 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 433 . . . . . . . . . 10  |-  ( ( z  e.  y  -> 
( y  e.  A  ->  z  e.  A ) )  ->  ( (
z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
18 pm3.3 432 . . . . . . . . . 10  |-  ( ( ( z  e.  y  /\  y  e.  A
)  ->  z  e.  A )  ->  (
z  e.  y  -> 
( y  e.  A  ->  z  e.  A ) ) )
1917, 18impbii 181 . . . . . . . . 9  |-  ( ( z  e.  y  -> 
( y  e.  A  ->  z  e.  A ) )  <->  ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
2016, 19syl6bb 253 . . . . . . . 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 247 . . . . . . 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 1632 . . . . . 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 245 . . . . 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 1632 . . . 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 245 . . 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 4238 . . 3  |-  ( Tr  A  <->  A. z A. y
( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
2725, 26syl6bbr 255 . 2  |-  ( A  e.  V  ->  ( [. A  /  x ]. A. z A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  Tr  A
) )
282, 27bitrd 245 1  |-  ( A  e.  V  ->  ( [. A  /  x ]. Tr  x  <->  Tr  A
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359   A.wal 1546    = wceq 1649    e. wcel 1717   [.wsbc 3097   Tr wtr 4236
This theorem is referenced by:  truniALT  27962  truniALTVD  28324  trintALTVD  28326  trintALT  28327
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-v 2894  df-sbc 3098  df-in 3263  df-ss 3270  df-uni 3951  df-tr 4237
  Copyright terms: Public domain W3C validator