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.

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

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