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

Theorem trsbc 27969
Description: Formula-building inference rule for class substitution, substituting a class variable for the set variable of the transitivity predicate. trsbc 27969 is trsbcVD 28331 without virtual deductions and was automatically derived from trsbcVD 28331 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 4246 . . 3  |-  ( Tr  x  <->  A. z A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
21sbcbiiOLD 3161 . 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 3153 . . . 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 3153 . . . . . 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 3161 . . . . . . . 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 27967 . . . . . . . . . 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 3137 . . . . . . . . . . 11  |-  ( A  e.  V  ->  ( [. A  /  x ]. z  e.  y  <->  z  e.  y ) )
12 sbcel2gv 3165 . . . . . . . . . . 11  |-  ( A  e.  V  ->  ( [. A  /  x ]. y  e.  x  <->  y  e.  A ) )
13 sbcel2gv 3165 . . . . . . . . . . 11  |-  ( A  e.  V  ->  ( [. A  /  x ]. z  e.  x  <->  z  e.  A ) )
14 imbi13 27948 . . . . . . . . . . 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 4246 . . 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 3105   Tr wtr 4244
This theorem is referenced by:  truniALT  27970  truniALTVD  28332  trintALTVD  28334  trintALT  28335
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 2369
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 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-v 2902  df-sbc 3106  df-in 3271  df-ss 3278  df-uni 3959  df-tr 4245
  Copyright terms: Public domain W3C validator