Theorem trsbc 44537

Description: Formula-building inference rule for class substitution, substituting a class variable for the setvar variable of the transitivity predicate. trsbc 44537 is trsbcVD 44873 without virtual deductions and was automatically derived from trsbcVD 44873 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 3816	. . 3 ⊢ ([𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑧[𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
2		sbcal 3816	. . . . 5 ⊢ ([𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦[𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
3		sbcim2g 44535	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ ([𝐴 / 𝑥]𝑧 ∈ 𝑦 → ([𝐴 / 𝑥]𝑦 ∈ 𝑥 → [𝐴 / 𝑥]𝑧 ∈ 𝑥))))
4		sbcg 3829	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦))
5		sbcel2gv 3823	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝐴))
6		sbcel2gv 3823	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝐴))
7		imbi13 44517	. . . . . . . . 9 ⊢ (([𝐴 / 𝑥]𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦) → (([𝐴 / 𝑥]𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝐴) → (([𝐴 / 𝑥]𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝐴) → (([𝐴 / 𝑥]𝑧 ∈ 𝑦 → ([𝐴 / 𝑥]𝑦 ∈ 𝑥 → [𝐴 / 𝑥]𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴))))))
8	4, 5, 6, 7	syl3c 66	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑉 → (([𝐴 / 𝑥]𝑧 ∈ 𝑦 → ([𝐴 / 𝑥]𝑦 ∈ 𝑥 → [𝐴 / 𝑥]𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴))))
9	3, 8	bitrd 279	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴))))
10		pm3.31 449	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
11		pm3.3 448	. . . . . . . . 9 ⊢ (((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) → (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)))
12	10, 11	impbii 209	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
13	12	sbcbii 3813	. . . . . . 7 ⊢ ([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ [𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
14		pm3.31 449	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴)) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))
15		pm3.3 448	. . . . . . . 8 ⊢ (((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴) → (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴)))
16	14, 15	impbii 209	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴)) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))
17	9, 13, 16	3bitr3g 313	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)))
18	17	albidv 1920	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (∀𝑦[𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)))
19	2, 18	bitrid 283	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)))
20	19	albidv 1920	. . 3 ⊢ (𝐴 ∈ 𝑉 → (∀𝑧[𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)))
21	1, 20	bitrid 283	. 2 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)))
22		dftr2 5219	. . 3 ⊢ (Tr 𝑥 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
23	22	sbcbii 3813	. 2 ⊢ ([𝐴 / 𝑥]Tr 𝑥 ↔ [𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
24		dftr2 5219	. 2 ⊢ (Tr 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))
25	21, 23, 24	3bitr4g 314	1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   ∈ wcel 2109  [wsbc 3756  Tr wtr 5217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-sbc 3757  df-ss 3934  df-uni 4875  df-tr 5218

This theorem is referenced by:  truniALT  44538  truniALTVD  44874  trintALTVD  44876  trintALT  44877