Theorem trsbc 31580

Description: Formula-building inference rule for class substitution, substituting a class variable for the setvar variable of the transitivity predicate. trsbc 31580 is trsbcVD 31946 without virtual deductions and was automatically derived from trsbcVD 31946 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 3346	. . 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 3346	. . . . 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 31578	. . . . . . . 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 3368	. . . . . . . . 9 |- ( A e. V -> ( [. A / x ]. z e. y <-> z e. y ) )
5		sbcel2gv 3361	. . . . . . . . 9 |- ( A e. V -> ( [. A / x ]. y e. x <-> y e. A ) )
6		sbcel2gv 3361	. . . . . . . . 9 |- ( A e. V -> ( [. A / x ]. z e. x <-> z e. A ) )
7		imbi13 31558	. . . . . . . . 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 445	. . . . . . . . 9 |- ( ( z e. y -> ( y e. x -> z e. x ) ) -> ( ( z e. y /\ y e. x ) -> z e. x ) )
11		pm3.3 444	. . . . . . . . 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 3354	. . . . . . 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 445	. . . . . . . 8 |- ( ( z e. y -> ( y e. A -> z e. A ) ) -> ( ( z e. y /\ y e. A ) -> z e. A ) )
15		pm3.3 444	. . . . . . . 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 1680	. . . . 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 1680	. . 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 4496	. . 3 |- ( Tr x <-> A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) )
23	22	sbcbii 3354	. 2 |- ( [. A / x ]. Tr x <-> [. A / x ]. A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) )
24		dftr2 4496	. 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 369   A.wal 1368   e. wcel 1758   [.wsbc 3294   Tr wtr 4494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-sbc 3295  df-in 3444  df-ss 3451  df-uni 4201  df-tr 4495

This theorem is referenced by:  truniALT  31581  truniALTVD  31947  trintALTVD  31949  trintALT  31950