Theorem tratrbVD 44077

Description: Virtual deduction proof of tratrb 43752. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)    ▶   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   )
2:1,?: e1a 43843	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   Tr 𝐴   )
3:1,?: e1a 43843	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)    ▶   ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
4:1,?: e1a 43843	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   𝐵 ∈ 𝐴   )
5::	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   )
6:5,?: e2 43847	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑥 ∈ 𝑦   )
7:5,?: e2 43847	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑦 ∈ 𝐵   )
8:2,7,4,?: e121 43872	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑦 ∈ 𝐴   )
9:2,6,8,?: e122 43869	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑥 ∈ 𝐴   )
10::	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵), 𝐵 ∈ 𝑥   ▶   𝐵 ∈ 𝑥   )
11:6,7,10,?: e223 43851	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵), 𝐵 ∈ 𝑥   ▶   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥)   )
12:11:	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   (𝐵 ∈ 𝑥 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥))   )
13::	⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥)
14:12,13,?: e20 43943	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   ¬ 𝐵 ∈ 𝑥   )
15::	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵), 𝑥 = 𝐵   ▶   𝑥 = 𝐵   )
16:7,15,?: e23 43971	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵), 𝑥 = 𝐵   ▶   𝑦 ∈ 𝑥   )
17:6,16,?: e23 43971	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵), 𝑥 = 𝐵   ▶   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)   )
18:17:	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   (𝑥 = 𝐵 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥))   )
19::	⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)
20:18,19,?: e20 43943	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   ¬ 𝑥 = 𝐵   )
21:3,?: e1a 43843	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
22:21,9,4,?: e121 43872	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   [𝑥 / 𝑥][𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
23:22,?: e2 43847	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   [𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
24:4,23,?: e12 43940	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   (𝑥 ∈ 𝐵 ∨ 𝐵 ∈ 𝑥 ∨ 𝑥 = 𝐵)   )
25:14,20,24,?: e222 43852	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑥 ∈ 𝐵   )
26:25:	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵)   )
27::	⊢ (∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑦∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
28:27,?: e0a 43988	⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → ∀𝑦(Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴))
29:28,26:	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)    ▶   ∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵)   )
30::	⊢ (∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑥∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
31:30,?: e0a 43988	⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → ∀𝑥(Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴))
32:31,29:	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑥 ∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵)   )
33:32,?: e1a 43843	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   Tr 𝐵   )
qed:33:	⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → Tr 𝐵)

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
tratrbVD	⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → Tr 𝐵)

Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦

Proof of Theorem tratrbVD

Step	Hyp	Ref	Expression
1		hbra1 3290	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑥∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
2		alrim3con13v 43749	. . . . 5 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑥∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)) → ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → ∀𝑥(Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)))
3	1, 2	e0a 43988	. . . 4 ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → ∀𝑥(Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴))
4		ax-5 1905	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 → ∀𝑦 𝑥 ∈ 𝐴)
5		hbra1 3290	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑦∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
6	4, 5	hbral 3297	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑦∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
7		alrim3con13v 43749	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑦∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)) → ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → ∀𝑦(Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)))
8	6, 7	e0a 43988	. . . . 5 ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → ∀𝑦(Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴))
9		idn2 43829	. . . . . . . . . . 11 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   )
10		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝑦)
11	9, 10	e2 43847	. . . . . . . . . 10 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑥 ∈ 𝑦   )
12		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵)
13	9, 12	e2 43847	. . . . . . . . . 10 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑦 ∈ 𝐵   )
14		idn3 43831	. . . . . . . . . 10 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ,   𝐵 ∈ 𝑥   ▶   𝐵 ∈ 𝑥   )
15		pm3.2an3 1337	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝑦 → (𝑦 ∈ 𝐵 → (𝐵 ∈ 𝑥 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥))))
16	11, 13, 14, 15	e223 43851	. . . . . . . . 9 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ,   𝐵 ∈ 𝑥   ▶   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥)   )
17	16	in3 43825	. . . . . . . 8 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   (𝐵 ∈ 𝑥 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥))   )
18		en3lp 9604	. . . . . . . 8 ⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥)
19		con3 153	. . . . . . . 8 ⊢ ((𝐵 ∈ 𝑥 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥)) → (¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥) → ¬ 𝐵 ∈ 𝑥))
20	17, 18, 19	e20 43943	. . . . . . 7 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶    ¬ 𝐵 ∈ 𝑥   )
21		idn3 43831	. . . . . . . . . . 11 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ,   𝑥 = 𝐵   ▶   𝑥 = 𝐵   )
22		eleq2 2814	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐵 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝐵))
23	22	biimprcd 249	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝐵 → (𝑥 = 𝐵 → 𝑦 ∈ 𝑥))
24	13, 21, 23	e23 43971	. . . . . . . . . 10 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ,   𝑥 = 𝐵   ▶   𝑦 ∈ 𝑥   )
25		pm3.2 469	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝑦 → (𝑦 ∈ 𝑥 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)))
26	11, 24, 25	e23 43971	. . . . . . . . 9 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ,   𝑥 = 𝐵   ▶   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)   )
27	26	in3 43825	. . . . . . . 8 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   (𝑥 = 𝐵 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥))   )
28		en2lp 9596	. . . . . . . 8 ⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)
29		con3 153	. . . . . . . 8 ⊢ ((𝑥 = 𝐵 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) → (¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → ¬ 𝑥 = 𝐵))
30	27, 28, 29	e20 43943	. . . . . . 7 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶    ¬ 𝑥 = 𝐵   )
31		idn1 43790	. . . . . . . . 9 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   )
32		simp3 1135	. . . . . . . . 9 ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ 𝐴)
33	31, 32	e1a 43843	. . . . . . . 8 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   𝐵 ∈ 𝐴   )
34		simp2 1134	. . . . . . . . . . . 12 ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
35	31, 34	e1a 43843	. . . . . . . . . . 11 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
36		ralcom 3278	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
37	36	biimpi 215	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
38	35, 37	e1a 43843	. . . . . . . . . 10 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
39		simp1 1133	. . . . . . . . . . . 12 ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → Tr 𝐴)
40	31, 39	e1a 43843	. . . . . . . . . . 11 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   Tr 𝐴   )
41		trel 5264	. . . . . . . . . . . . 13 ⊢ (Tr 𝐴 → ((𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴) → 𝑦 ∈ 𝐴))
42	41	expd 415	. . . . . . . . . . . 12 ⊢ (Tr 𝐴 → (𝑦 ∈ 𝐵 → (𝐵 ∈ 𝐴 → 𝑦 ∈ 𝐴)))
43	40, 13, 33, 42	e121 43872	. . . . . . . . . . 11 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑦 ∈ 𝐴   )
44		trel 5264	. . . . . . . . . . . 12 ⊢ (Tr 𝐴 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴))
45	44	expd 415	. . . . . . . . . . 11 ⊢ (Tr 𝐴 → (𝑥 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑥 ∈ 𝐴)))
46	40, 11, 43, 45	e122 43869	. . . . . . . . . 10 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑥 ∈ 𝐴   )
47		rspsbc2 43750	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝐴 → (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → [𝑥 / 𝑥][𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))))
48	47	com13 88	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → (𝑥 ∈ 𝐴 → (𝐵 ∈ 𝐴 → [𝑥 / 𝑥][𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))))
49	38, 46, 33, 48	e121 43872	. . . . . . . . 9 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   [𝑥 / 𝑥][𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
50		equid 2007	. . . . . . . . . . 11 ⊢ 𝑥 = 𝑥
51		sbceq2a 3781	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑥 → ([𝑥 / 𝑥][𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ↔ [𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)))
52	50, 51	ax-mp 5	. . . . . . . . . 10 ⊢ ([𝑥 / 𝑥][𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ↔ [𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
53	52	biimpi 215	. . . . . . . . 9 ⊢ ([𝑥 / 𝑥][𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → [𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
54	49, 53	e2 43847	. . . . . . . 8 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   [𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
55		sbcoreleleq 43751	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝐴 → ([𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ↔ (𝑥 ∈ 𝐵 ∨ 𝐵 ∈ 𝑥 ∨ 𝑥 = 𝐵)))
56	55	biimpd 228	. . . . . . . 8 ⊢ (𝐵 ∈ 𝐴 → ([𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → (𝑥 ∈ 𝐵 ∨ 𝐵 ∈ 𝑥 ∨ 𝑥 = 𝐵)))
57	33, 54, 56	e12 43940	. . . . . . 7 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   (𝑥 ∈ 𝐵 ∨ 𝐵 ∈ 𝑥 ∨ 𝑥 = 𝐵)   )
58		3ornot23 43725	. . . . . . . 8 ⊢ ((¬ 𝐵 ∈ 𝑥 ∧ ¬ 𝑥 = 𝐵) → ((𝑥 ∈ 𝐵 ∨ 𝐵 ∈ 𝑥 ∨ 𝑥 = 𝐵) → 𝑥 ∈ 𝐵))
59	58	ex 412	. . . . . . 7 ⊢ (¬ 𝐵 ∈ 𝑥 → (¬ 𝑥 = 𝐵 → ((𝑥 ∈ 𝐵 ∨ 𝐵 ∈ 𝑥 ∨ 𝑥 = 𝐵) → 𝑥 ∈ 𝐵)))
60	20, 30, 57, 59	e222 43852	. . . . . 6 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑥 ∈ 𝐵   )
61	60	in2 43821	. . . . 5 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵)   )
62	8, 61	gen11nv 43833	. . . 4 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵)   )
63	3, 62	gen11nv 43833	. . 3 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵)   )
64		dftr2 5257	. . . 4 ⊢ (Tr 𝐵 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵))
65	64	biimpri 227	. . 3 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵) → Tr 𝐵)
66	63, 65	e1a 43843	. 2 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   Tr 𝐵   )
67	66	in1 43787	1 ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → Tr 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∨ w3o 1083   ∧ w3a 1084  ∀wal 1531   = wceq 1533   ∈ wcel 2098  ∀wral 3053  [wsbc 3769  Tr wtr 5255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pr 5417  ax-un 7718  ax-reg 9582

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-sbc 3770  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-uni 4900  df-br 5139  df-opab 5201  df-tr 5256  df-eprel 5570  df-fr 5621  df-vd1 43786  df-vd2 43794  df-vd3 43806

This theorem is referenced by: (None)