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\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\mathrm{Tr}x\leftrightarrow \mathrm{Tr}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		sbcal	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall z\forall y\left(\left(z\in y\wedge y\in x\right)\to z\in x\right)\leftrightarrow \forall z\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\left(\left(z\in y\wedge y\in x\right)\to z\in x\right)$$
2		sbcal	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\left(\left(z\in y\wedge y\in x\right)\to z\in x\right)\leftrightarrow \forall y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\left(z\in y\wedge y\in x\right)\to z\in x\right)$$
3		sbcim2g	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\in y\to \left(y\in x\to z\in x\right)\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in y\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in x\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in x\right)\right)\right)$$
4		sbcg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in y\leftrightarrow z\in y\right)$$
5		sbcel2gv	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in x\leftrightarrow y\in A\right)$$
6		sbcel2gv	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in x\leftrightarrow z\in A\right)$$
7		imbi13	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in y\leftrightarrow z\in y\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in x\leftrightarrow y\in A\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in x\leftrightarrow z\in A\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in y\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in x\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in x\right)\right)\leftrightarrow \left(z\in y\to \left(y\in A\to z\in A\right)\right)\right)\right)\right)$$
8	4 5 6 7	syl3c	$$⊢A\in V\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in y\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in x\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in x\right)\right)\leftrightarrow \left(z\in y\to \left(y\in A\to z\in A\right)\right)\right)$$
9	3 8	bitrd	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\in y\to \left(y\in x\to z\in x\right)\right)\leftrightarrow \left(z\in y\to \left(y\in A\to z\in A\right)\right)\right)$$
10		pm3.31	$$⊢\left(z\in y\to \left(y\in x\to z\in x\right)\right)\to \left(\left(z\in y\wedge y\in x\right)\to z\in x\right)$$
11		pm3.3	$$⊢\left(\left(z\in y\wedge y\in x\right)\to z\in x\right)\to \left(z\in y\to \left(y\in x\to z\in x\right)\right)$$
12	10 11	impbii	$$⊢\left(z\in y\to \left(y\in x\to z\in x\right)\right)\leftrightarrow \left(\left(z\in y\wedge y\in x\right)\to z\in x\right)$$
13	12	sbcbii	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\in y\to \left(y\in x\to z\in x\right)\right)\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\left(z\in y\wedge y\in x\right)\to z\in x\right)$$
14		pm3.31	$$⊢\left(z\in y\to \left(y\in A\to z\in A\right)\right)\to \left(\left(z\in y\wedge y\in A\right)\to z\in A\right)$$
15		pm3.3	$$⊢\left(\left(z\in y\wedge y\in A\right)\to z\in A\right)\to \left(z\in y\to \left(y\in A\to z\in A\right)\right)$$
16	14 15	impbii	$$⊢\left(z\in y\to \left(y\in A\to z\in A\right)\right)\leftrightarrow \left(\left(z\in y\wedge y\in A\right)\to z\in A\right)$$
17	9 13 16	3bitr3g	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\left(z\in y\wedge y\in x\right)\to z\in x\right)\leftrightarrow \left(\left(z\in y\wedge y\in A\right)\to z\in A\right)\right)$$
18	17	albidv	$$⊢A\in V\to \left(\forall y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\left(z\in y\wedge y\in x\right)\to z\in x\right)\leftrightarrow \forall y\left(\left(z\in y\wedge y\in A\right)\to z\in A\right)\right)$$
19	2 18	bitrid	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\left(\left(z\in y\wedge y\in x\right)\to z\in x\right)\leftrightarrow \forall y\left(\left(z\in y\wedge y\in A\right)\to z\in A\right)\right)$$
20	19	albidv	$$⊢A\in V\to \left(\forall z\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\left(\left(z\in y\wedge y\in x\right)\to z\in x\right)\leftrightarrow \forall z\forall y\left(\left(z\in y\wedge y\in A\right)\to z\in A\right)\right)$$
21	1 20	bitrid	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall z\forall y\left(\left(z\in y\wedge y\in x\right)\to z\in x\right)\leftrightarrow \forall z\forall y\left(\left(z\in y\wedge y\in A\right)\to z\in A\right)\right)$$
22		dftr2	$$⊢\mathrm{Tr}x\leftrightarrow \forall z\forall y\left(\left(z\in y\wedge y\in x\right)\to z\in x\right)$$
23	22	sbcbii	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\mathrm{Tr}x\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall z\forall y\left(\left(z\in y\wedge y\in x\right)\to z\in x\right)$$
24		dftr2	$$⊢\mathrm{Tr}A\leftrightarrow \forall z\forall y\left(\left(z\in y\wedge y\in A\right)\to z\in A\right)$$
25	21 23 24	3bitr4g	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\mathrm{Tr}x\leftrightarrow \mathrm{Tr}A\right)$$