Theorem trsbc 45725

Description: Formula-building inference rule for class substitution, substituting a class variable for the setvar variable of the transitivity predicate. trsbc 45725 is trsbcVD 46061 without virtual deductions and was automatically derived from trsbcVD 46061 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 3801	. . 3 ⊢ ([𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑧[𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
2		sbcal 3801	. . . . 5 ⊢ ([𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦[𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
3		sbcim2g 45723	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ ([𝐴 / 𝑥]𝑧 ∈ 𝑦 → ([𝐴 / 𝑥]𝑦 ∈ 𝑥 → [𝐴 / 𝑥]𝑧 ∈ 𝑥))))
4		sbcg 3814	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦))
5		sbcel2gv 3808	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝐴))
6		sbcel2gv 3808	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝐴))
7		imbi13 45705	. . . . . . . . 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 3798	. . . . . . 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 1955	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (∀𝑦[𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)))
19	2, 18	bitrid 286	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)))
20	19	albidv 1955	. . 3 ⊢ (𝐴 ∈ 𝑉 → (∀𝑧[𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)))
21	1, 20	bitrid 286	. 2 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)))
22		dftr2 5218	. . 3 ⊢ (Tr 𝑥 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
23	22	sbcbii 3798	. 2 ⊢ ([𝐴 / 𝑥]Tr 𝑥 ↔ [𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
24		dftr2 5218	. 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 2147  [wsbc 3742  Tr wtr 5216

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-sbc 3743  df-ss 3901  df-uni 4871  df-tr 5217

This theorem is used by:  truniALT  45726  truniALTVD  46062  trintALTVD  46064  trintALT  46065