Theorem trsbcVD

Description: Formula-building inference rule for class substitution, substituting a class variable for the setvar variable of the transitivity predicate. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. trsbc is trsbcVD without virtual deductions and was automatically derived from trsbcVD .

	Ref	Expression
Assertion	trsbcVD	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\mathrm{Tr}x\leftrightarrow \mathrm{Tr}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		idn1	$$⊢\left(A\in B\to A\in B\right)$$
2		sbcg	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in y\leftrightarrow z\in y\right)$$
3	1 2	e1a	$$⊢\left(A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in y\leftrightarrow z\in y\right)\right)$$
4		sbcel2gv	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in x\leftrightarrow y\in A\right)$$
5	1 4	e1a	$$⊢\left(A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in x\leftrightarrow y\in A\right)\right)$$
6		sbcel2gv	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in x\leftrightarrow z\in A\right)$$
7	1 6	e1a	$$⊢\left(A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in x\leftrightarrow z\in A\right)\right)$$
8		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)$$
9	8	a1i	$$⊢A\in B\to \left(\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)\right)$$
10	1 3 5 7 9	e1111	$$⊢\left(A\in B\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)$$
11		sbcim2g	$$⊢A\in B\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)$$
12	1 11	e1a	$$⊢\left(A\in B\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)\right)$$
13		bibi1	$$⊢\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)\to \left(\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)\leftrightarrow \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)$$
14	13	biimprcd	$$⊢\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)\to \left(\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)\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)\right)$$
15	10 12 14	e11	$$⊢\left(A\in B\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)\right)$$
16		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)$$
17		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)$$
18	16 17	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)$$
19		bibi1	$$⊢\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)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\in y\to \left(y\in x\to z\in x\right)\right)\leftrightarrow \left(\left(z\in y\wedge y\in A\right)\to z\in A\right)\right)\leftrightarrow \left(\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)\right)\right)$$
20	19	biimprd	$$⊢\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)\to \left(\left(\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)\right)\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(\left(z\in y\wedge y\in A\right)\to z\in A\right)\right)\right)$$
21	15 18 20	e10	$$⊢\left(A\in B\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(\left(z\in y\wedge y\in A\right)\to z\in A\right)\right)\right)$$
22		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)$$
23		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)$$
24	22 23	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)$$
25	24	ax-gen	$$⊢\forall x\left(\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)\right)$$
26		sbcbi	$$⊢A\in B\to \left(\forall x\left(\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)\right)\to \left(\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)\right)\right)$$
27	1 25 26	e10	$$⊢\left(A\in B\to \left(\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)\right)\right)$$
28		bitr3	$$⊢\left(\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)\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\in y\to \left(y\in x\to z\in x\right)\right)\leftrightarrow \left(\left(z\in y\wedge y\in A\right)\to z\in A\right)\right)\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)\right)$$
29	28	com12	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\in y\to \left(y\in x\to z\in x\right)\right)\leftrightarrow \left(\left(z\in y\wedge y\in A\right)\to z\in A\right)\right)\to \left(\left(\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)\right)\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)\right)$$
30	21 27 29	e11	$$⊢\left(A\in B\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)\right)$$
31	30	gen11	$$⊢\left(A\in B\to \forall y\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)\right)$$
32		albi	$$⊢\forall y\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)\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)$$
33	31 32	e1a	$$⊢\left(A\in B\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)\right)$$
34		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)$$
35	34	a1i	$$⊢A\in B\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\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\left(z\in y\wedge y\in x\right)\to z\in x\right)\right)$$
36	1 35	e1a	$$⊢\left(A\in B\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\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\left(z\in y\wedge y\in x\right)\to z\in x\right)\right)\right)$$
37		bibi1	$$⊢\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\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\left(z\in y\wedge y\in x\right)\to z\in x\right)\right)\to \left(\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)\leftrightarrow \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)\right)$$
38	37	biimprcd	$$⊢\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)\to \left(\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\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\left(z\in y\wedge y\in x\right)\to z\in x\right)\right)\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)\right)$$
39	33 36 38	e11	$$⊢\left(A\in B\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)\right)$$
40	39	gen11	$$⊢\left(A\in B\to \forall z\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)\right)$$
41		albi	$$⊢\forall z\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)\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)$$
42	40 41	e1a	$$⊢\left(A\in B\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)\right)$$
43		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)$$
44	43	a1i	$$⊢A\in B\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\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\left(\left(z\in y\wedge y\in x\right)\to z\in x\right)\right)$$
45	1 44	e1a	$$⊢\left(A\in B\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\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\left(\left(z\in y\wedge y\in x\right)\to z\in x\right)\right)\right)$$
46		bibi1	$$⊢\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\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\left(\left(z\in y\wedge y\in x\right)\to z\in x\right)\right)\to \left(\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)\leftrightarrow \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)\right)$$
47	46	biimprcd	$$⊢\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)\to \left(\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\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\left(\left(z\in y\wedge y\in x\right)\to z\in x\right)\right)\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)\right)$$
48	42 45 47	e11	$$⊢\left(A\in B\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)\right)$$
49		dftr2	$$⊢\mathrm{Tr}A\leftrightarrow \forall z\forall y\left(\left(z\in y\wedge y\in A\right)\to z\in A\right)$$
50		biantr	$$⊢\left(\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)\wedge \left(\mathrm{Tr}A\leftrightarrow \forall z\forall y\left(\left(z\in y\wedge y\in A\right)\to z\in A\right)\right)\right)\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 \mathrm{Tr}A\right)$$
51	50	ex	$$⊢\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)\to \left(\left(\mathrm{Tr}A\leftrightarrow \forall z\forall y\left(\left(z\in y\wedge y\in A\right)\to z\in A\right)\right)\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 \mathrm{Tr}A\right)\right)$$
52	48 49 51	e10	$$⊢\left(A\in B\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 \mathrm{Tr}A\right)\right)$$
53		dftr2	$$⊢\mathrm{Tr}x\leftrightarrow \forall z\forall y\left(\left(z\in y\wedge y\in x\right)\to z\in x\right)$$
54	53	ax-gen	$$⊢\forall x\left(\mathrm{Tr}x\leftrightarrow \forall z\forall y\left(\left(z\in y\wedge y\in x\right)\to z\in x\right)\right)$$
55		sbcbi	$$⊢A\in B\to \left(\forall x\left(\mathrm{Tr}x\leftrightarrow \forall z\forall y\left(\left(z\in y\wedge y\in x\right)\to z\in x\right)\right)\to \left(\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)\right)\right)$$
56	1 54 55	e10	$$⊢\left(A\in B\to \left(\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)\right)\right)$$
57		bibi1	$$⊢\left(\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)\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\mathrm{Tr}x\leftrightarrow \mathrm{Tr}A\right)\leftrightarrow \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 \mathrm{Tr}A\right)\right)$$
58	57	biimprcd	$$⊢\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 \mathrm{Tr}A\right)\to \left(\left(\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)\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\mathrm{Tr}x\leftrightarrow \mathrm{Tr}A\right)\right)$$
59	52 56 58	e11	$$⊢\left(A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\mathrm{Tr}x\leftrightarrow \mathrm{Tr}A\right)\right)$$
60	59	in1	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\mathrm{Tr}x\leftrightarrow \mathrm{Tr}A\right)$$