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

Theorem trsbc 33686
Description: Formula-building inference rule for class substitution, substituting a class variable for the setvar variable of the transitivity predicate. trsbc 33686 is trsbcVD 34063 without virtual deductions and was automatically derived from trsbcVD 34063 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 3319 . . 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 3319 . . . . 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 33684 . . . . . . . 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 3335 . . . . . . . . 9  |-  ( A  e.  V  ->  ( [. A  /  x ]. z  e.  y  <->  z  e.  y ) )
5 sbcel2gv 3329 . . . . . . . . 9  |-  ( A  e.  V  ->  ( [. A  /  x ]. y  e.  x  <->  y  e.  A ) )
6 sbcel2gv 3329 . . . . . . . . 9  |-  ( A  e.  V  ->  ( [. A  /  x ]. z  e.  x  <->  z  e.  A ) )
7 imbi13 33662 . . . . . . . . 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 61 . . . . . . . 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 253 . . . . . . 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 443 . . . . . . . . 9  |-  ( ( z  e.  y  -> 
( y  e.  x  ->  z  e.  x ) )  ->  ( (
z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
11 pm3.3 442 . . . . . . . . 9  |-  ( ( ( z  e.  y  /\  y  e.  x
)  ->  z  e.  x )  ->  (
z  e.  y  -> 
( y  e.  x  ->  z  e.  x ) ) )
1210, 11impbii 188 . . . . . . . 8  |-  ( ( z  e.  y  -> 
( y  e.  x  ->  z  e.  x ) )  <->  ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
1312sbcbii 3325 . . . . . . 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 443 . . . . . . . 8  |-  ( ( z  e.  y  -> 
( y  e.  A  ->  z  e.  A ) )  ->  ( (
z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
15 pm3.3 442 . . . . . . . 8  |-  ( ( ( z  e.  y  /\  y  e.  A
)  ->  z  e.  A )  ->  (
z  e.  y  -> 
( y  e.  A  ->  z  e.  A ) ) )
1614, 15impbii 188 . . . . . . 7  |-  ( ( z  e.  y  -> 
( y  e.  A  ->  z  e.  A ) )  <->  ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
179, 13, 163bitr3g 287 . . . . . 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 1728 . . . . 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 257 . . . 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 1728 . . 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 257 . 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 4479 . . 3  |-  ( Tr  x  <->  A. z A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
2322sbcbii 3325 . 2  |-  ( [. A  /  x ]. Tr  x 
<-> 
[. A  /  x ]. A. z A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
24 dftr2 4479 . 2  |-  ( Tr  A  <->  A. z A. y
( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
2521, 23, 243bitr4g 288 1  |-  ( A  e.  V  ->  ( [. A  /  x ]. Tr  x  <->  Tr  A
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367   A.wal 1397    e. wcel 1836   [.wsbc 3269   Tr wtr 4477
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-v 3053  df-sbc 3270  df-in 3413  df-ss 3420  df-uni 4181  df-tr 4478
This theorem is referenced by:  truniALT  33687  truniALTVD  34064  trintALTVD  34066  trintALT  34067
  Copyright terms: Public domain W3C validator