Metamath Proof Explorer

Theorem trsbc

Description: Formula-building inference rule for class substitution, substituting a class variable for the setvar variable of the transitivity predicate. trsbc is trsbcVD without virtual deductions and was automatically derived from trsbcVD 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.)

Ref Expression
Assertion trsbc 
|- ( A e. V -> ( [. A / x ]. Tr x <-> Tr A ) )

Proof

Step Hyp Ref Expression
1 sbcal 
 |-  ( [. 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 
 |-  ( [. 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 
 |-  ( 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 
 |-  ( A e. V -> ( [. A / x ]. z e. y <-> z e. y ) )
5 sbcel2gv 
 |-  ( A e. V -> ( [. A / x ]. y e. x <-> y e. A ) )
6 sbcel2gv 
 |-  ( A e. V -> ( [. A / x ]. z e. x <-> z e. A ) )
7 imbi13 
 |-  ( ( [. 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 ) ) ) ) ) )
8 4 5 6 7 syl3c 
 |-  ( 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 ) ) ) )
9 3 8 bitrd 
 |-  ( 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 
 |-  ( ( z e. y -> ( y e. x -> z e. x ) ) -> ( ( z e. y /\ y e. x ) -> z e. x ) )
11 pm3.3 
 |-  ( ( ( z e. y /\ y e. x ) -> z e. x ) -> ( z e. y -> ( y e. x -> z e. x ) ) )
12 10 11 impbii 
 |-  ( ( z e. y -> ( y e. x -> z e. x ) ) <-> ( ( z e. y /\ y e. x ) -> z e. x ) )
13 12 sbcbii 
 |-  ( [. 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 
 |-  ( ( z e. y -> ( y e. A -> z e. A ) ) -> ( ( z e. y /\ y e. A ) -> z e. A ) )
15 pm3.3 
 |-  ( ( ( z e. y /\ y e. A ) -> z e. A ) -> ( z e. y -> ( y e. A -> z e. A ) ) )
16 14 15 impbii 
 |-  ( ( z e. y -> ( y e. A -> z e. A ) ) <-> ( ( z e. y /\ y e. A ) -> z e. A ) )
17 9 13 16 3bitr3g 
 |-  ( A e. V -> ( [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) <-> ( ( z e. y /\ y e. A ) -> z e. A ) ) )
18 17 albidv 
 |-  ( 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 ) ) )
19 2 18 syl5bb 
 |-  ( 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 ) ) )
20 19 albidv 
 |-  ( 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 ) ) )
21 1 20 syl5bb 
 |-  ( 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 
 |-  ( Tr x <-> A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) )
23 22 sbcbii 
 |-  ( [. A / x ]. Tr x <-> [. A / x ]. A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) )
24 dftr2 
 |-  ( Tr A <-> A. z A. y ( ( z e. y /\ y e. A ) -> z e. A ) )
25 21 23 24 3bitr4g 
 |-  ( A e. V -> ( [. A / x ]. Tr x <-> Tr A ) )