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.

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

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