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	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] Tr 𝑥 ↔ Tr 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		sbcal	⊢ ( [ 𝐴 / 𝑥 ] ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑧 [ 𝐴 / 𝑥 ] ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
2		sbcal	⊢ ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑦 [ 𝐴 / 𝑥 ] ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
3		sbcim2g	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑥 → [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑥 ) ) ) )
4		sbcg	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦 ) )
5		sbcel2gv	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝐴 ) )
6		sbcel2gv	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝐴 ) )
7		imbi13	⊢ ( ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦 ) → ( ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝐴 ) → ( ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝐴 ) → ( ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑥 → [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑥 ) ) ↔ ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ) ) ) ) )
8	4 5 6 7	syl3c	⊢ ( 𝐴 ∈ 𝑉 → ( ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑥 → [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑥 ) ) ↔ ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ) ) )
9	3 8	bitrd	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) ↔ ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ) ) )
10		pm3.31	⊢ ( ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
11		pm3.3	⊢ ( ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) → ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) )
12	10 11	impbii	⊢ ( ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) ↔ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
13	12	sbcbii	⊢ ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) ↔ [ 𝐴 / 𝑥 ] ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
14		pm3.31	⊢ ( ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ) → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )
15		pm3.3	⊢ ( ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) → ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ) )
16	14 15	impbii	⊢ ( ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ) ↔ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )
17	9 13 16	3bitr3g	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) )
18	17	albidv	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑦 [ 𝐴 / 𝑥 ] ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) )
19	2 18	syl5bb	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) )
20	19	albidv	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑧 [ 𝐴 / 𝑥 ] ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) )
21	1 20	syl5bb	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) )
22		dftr2	⊢ ( Tr 𝑥 ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
23	22	sbcbii	⊢ ( [ 𝐴 / 𝑥 ] Tr 𝑥 ↔ [ 𝐴 / 𝑥 ] ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
24		dftr2	⊢ ( Tr 𝐴 ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )
25	21 23 24	3bitr4g	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] Tr 𝑥 ↔ Tr 𝐴 ) )