Theorem trsbc 45482

Description: Formula-building inference rule for class substitution, substituting a class variable for the setvar variable of the transitivity predicate. trsbc 45482 is trsbcVD 45818 without virtual deductions and was automatically derived from trsbcVD 45818 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	⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴))

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝑉(𝑥)

Proof of Theorem trsbc

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sbcal 3798	. . 3 ⊢ ([𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑧[𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
2		sbcal 3798	. . . . 5 ⊢ ([𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦[𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
3		sbcim2g 45480	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ ([𝐴 / 𝑥]𝑧 ∈ 𝑦 → ([𝐴 / 𝑥]𝑦 ∈ 𝑥 → [𝐴 / 𝑥]𝑧 ∈ 𝑥))))
4		sbcg 3811	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦))
5		sbcel2gv 3805	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝐴))
6		sbcel2gv 3805	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝐴))
7		imbi13 45462	. . . . . . . . 9 ⊢ (([𝐴 / 𝑥]𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦) → (([𝐴 / 𝑥]𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝐴) → (([𝐴 / 𝑥]𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝐴) → (([𝐴 / 𝑥]𝑧 ∈ 𝑦 → ([𝐴 / 𝑥]𝑦 ∈ 𝑥 → [𝐴 / 𝑥]𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴))))))
8	4, 5, 6, 7	syl3c 67	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑉 → (([𝐴 / 𝑥]𝑧 ∈ 𝑦 → ([𝐴 / 𝑥]𝑦 ∈ 𝑥 → [𝐴 / 𝑥]𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴))))
9	3, 8	bitrd 282	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴))))
10		pm3.31 455	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
11		pm3.3 454	. . . . . . . . 9 ⊢ (((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) → (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)))
12	10, 11	impbii 212	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
13	12	sbcbii 3795	. . . . . . 7 ⊢ ([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ [𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
14		pm3.31 455	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴)) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))
15		pm3.3 454	. . . . . . . 8 ⊢ (((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴) → (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴)))
16	14, 15	impbii 212	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴)) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))
17	9, 13, 16	3bitr3g 316	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)))
18	17	albidv 1953	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (∀𝑦[𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)))
19	2, 18	bitrid 286	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)))
20	19	albidv 1953	. . 3 ⊢ (𝐴 ∈ 𝑉 → (∀𝑧[𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)))
21	1, 20	bitrid 286	. 2 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)))
22		dftr2 5214	. . 3 ⊢ (Tr 𝑥 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
23	22	sbcbii 3795	. 2 ⊢ ([𝐴 / 𝑥]Tr 𝑥 ↔ [𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
24		dftr2 5214	. 2 ⊢ (Tr 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))
25	21, 23, 24	3bitr4g 317	1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   ∈ wcel 2145  [wsbc 3739  Tr wtr 5212

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-sbc 3740  df-ss 3916  df-uni 4868  df-tr 5213

This theorem is used by:  truniALT  45483  truniALTVD  45819  trintALTVD  45821  trintALT  45822