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

Theorem trsbc 36946
Description: Formula-building inference rule for class substitution, substituting a class variable for the setvar variable of the transitivity predicate. trsbc 36946 is trsbcVD 37315 without virtual deductions and was automatically derived from trsbcVD 37315 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 sbcal 3329 . . 3  |-  ( [. 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 ) )
2 sbcal 3329 . . . . 5  |-  ( [. 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 ) )
3 sbcim2g 36944 . . . . . . . 8  |-  ( 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 ) ) ) )
4 sbcg 3345 . . . . . . . . 9  |-  ( A  e.  V  ->  ( [. A  /  x ]. z  e.  y  <->  z  e.  y ) )
5 sbcel2gv 3339 . . . . . . . . 9  |-  ( A  e.  V  ->  ( [. A  /  x ]. y  e.  x  <->  y  e.  A ) )
6 sbcel2gv 3339 . . . . . . . . 9  |-  ( A  e.  V  ->  ( [. A  /  x ]. z  e.  x  <->  z  e.  A ) )
7 imbi13 36922 . . . . . . . . 9  |-  ( (
[. 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 ) ) ) ) ) )
84, 5, 6, 7syl3c 63 . . . . . . . 8  |-  ( 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 ) ) ) )
93, 8bitrd 261 . . . . . . 7  |-  ( A  e.  V  ->  ( [. A  /  x ]. ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( z  e.  y  ->  ( y  e.  A  ->  z  e.  A ) ) ) )
10 pm3.31 451 . . . . . . . . 9  |-  ( ( z  e.  y  -> 
( y  e.  x  ->  z  e.  x ) )  ->  ( (
z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
11 pm3.3 450 . . . . . . . . 9  |-  ( ( ( z  e.  y  /\  y  e.  x
)  ->  z  e.  x )  ->  (
z  e.  y  -> 
( y  e.  x  ->  z  e.  x ) ) )
1210, 11impbii 192 . . . . . . . 8  |-  ( ( z  e.  y  -> 
( y  e.  x  ->  z  e.  x ) )  <->  ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
1312sbcbii 3335 . . . . . . 7  |-  ( [. A  /  x ]. (
z  e.  y  -> 
( y  e.  x  ->  z  e.  x ) )  <->  [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
14 pm3.31 451 . . . . . . . 8  |-  ( ( z  e.  y  -> 
( y  e.  A  ->  z  e.  A ) )  ->  ( (
z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
15 pm3.3 450 . . . . . . . 8  |-  ( ( ( z  e.  y  /\  y  e.  A
)  ->  z  e.  A )  ->  (
z  e.  y  -> 
( y  e.  A  ->  z  e.  A ) ) )
1614, 15impbii 192 . . . . . . 7  |-  ( ( z  e.  y  -> 
( y  e.  A  ->  z  e.  A ) )  <->  ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
179, 13, 163bitr3g 295 . . . . . 6  |-  ( A  e.  V  ->  ( [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  ( (
z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) )
1817albidv 1778 . . . . 5  |-  ( 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 ) ) )
192, 18syl5bb 265 . . . 4  |-  ( 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 ) ) )
2019albidv 1778 . . 3  |-  ( 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 ) ) )
211, 20syl5bb 265 . 2  |-  ( 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 ) ) )
22 dftr2 4515 . . 3  |-  ( Tr  x  <->  A. z A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
2322sbcbii 3335 . 2  |-  ( [. A  /  x ]. Tr  x 
<-> 
[. A  /  x ]. A. z A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
24 dftr2 4515 . 2  |-  ( Tr  A  <->  A. z A. y
( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
2521, 23, 243bitr4g 296 1  |-  ( A  e.  V  ->  ( [. A  /  x ]. Tr  x  <->  Tr  A
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375   A.wal 1453    e. wcel 1898   [.wsbc 3279   Tr wtr 4513
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-sbc 3280  df-in 3423  df-ss 3430  df-uni 4213  df-tr 4514
This theorem is referenced by:  truniALT  36947  truniALTVD  37316  trintALTVD  37318  trintALT  37319
  Copyright terms: Public domain W3C validator