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 (\underset{˙}{[} A / x \underset{˙}{]} Tr x \leftrightarrow Tr A)$

Proof

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

1::	\|- (. A e. B ->. A e. B ).
2:1:	\|- (. A e. B ->. ( [. A / x ]. z e. y <-> z e. y ) ).
3:1:	\|- (. A e. B ->. ( [. A / x ]. y e. x <-> y e. A ) ).
4:1:	\|- (. A e. B ->. ( [. A / x ]. z e. x <-> z e. A ) ).
5:1,2,3,4:	\|- (. A e. B ->. ( ( [. A / x ]. z e. y -> ( [. A / x ]. y e. x -> [. A / x ]. z e. x ) ) <-> ( z e. y -> ( y e. A -> z e. A ) ) ) ).
6:1:	\|- (. A e. B ->. ( [. 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 ) ) ) ).
7:5,6:	\|- (. A e. B ->. ( [. A / x ]. ( z e. y -> ( y e. x -> z e. x ) ) <-> ( z e. y -> ( y e. A -> z e. A ) ) ) ).
8::	\|- ( ( z e. y -> ( y e. A -> z e. A ) ) <-> ( ( z e. y /\ y e. A ) -> z e. A ) )
9:7,8:	\|- (. A e. B ->. ( [. A / x ]. ( z e. y -> ( y e. x -> z e. x ) ) <-> ( ( z e. y /\ y e. A ) -> z e. A ) ) ).
10::	\|- ( ( z e. y -> ( y e. x -> z e. x ) ) <-> ( ( z e. y /\ y e. x ) -> z e. x ) )
11:10:	\|- A. x ( ( z e. y -> ( y e. x -> z e. x ) ) <-> ( ( z e. y /\ y e. x ) -> z e. x ) )
12:1,11:	\|- (. A e. B ->. ( [. A / x ]. ( z e. y -> ( y e. x -> z e. x ) ) <-> [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) ) ).
13:9,12:	\|- (. A e. B ->. ( [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) <-> ( ( z e. y /\ y e. A ) -> z e. A ) ) ).
14:13:	\|- (. A e. B ->. A. y ( [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) <-> ( ( z e. y /\ y e. A ) -> z e. A ) ) ).
15:14:	\|- (. A e. B ->. ( A. y [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) ).
16:1:	\|- (. A e. B ->. ( [. 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 ) ) ).
17:15,16:	\|- (. A e. B ->. ( [. A / x ]. A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) ).
18:17:	\|- (. A e. B ->. A. z ( [. A / x ]. A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) ).
19:18:	\|- (. A e. B ->. ( 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 ) ) ).
20:1:	\|- (. A e. B ->. ( [. 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 ) ) ).
21:19,20:	\|- (. A e. B ->. ( [. 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::	\|- ( Tr A <-> A. z A. y ( ( z e. y /\ y e. A ) -> z e. A ) )
23:21,22:	\|- (. A e. B ->. ( [. A / x ]. A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> Tr A ) ).
24::	\|- ( Tr x <-> A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) )
25:24:	\|- A. x ( Tr x <-> A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) )
26:1,25:	\|- (. A e. B ->. ( [. A / x ]. Tr x <-> [. A / x ]. A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) ) ).
27:23,26:	\|- (. A e. B ->. ( [. A / x ]. Tr x <-> Tr A ) ).
qed:27:	\|- ( A e. B -> ( [. A / x ]. Tr x <-> Tr A ) )

Metamath Proof Explorer

Theorem trsbcVD

Proof