Theorem tratrbVD 41188

Description: Virtual deduction proof of tratrb 40863. 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 40954	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   Tr 𝐴   )
3:1,?: e1a 40954	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)    ▶   ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
4:1,?: e1a 40954	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   𝐵 ∈ 𝐴   )
5::	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   )
6:5,?: e2 40958	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑥 ∈ 𝑦   )
7:5,?: e2 40958	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑦 ∈ 𝐵   )
8:2,7,4,?: e121 40983	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑦 ∈ 𝐴   )
9:2,6,8,?: e122 40980	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑥 ∈ 𝐴   )
10::	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵), 𝐵 ∈ 𝑥   ▶   𝐵 ∈ 𝑥   )
11:6,7,10,?: e223 40962	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵), 𝐵 ∈ 𝑥   ▶   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥)   )
12:11:	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   (𝐵 ∈ 𝑥 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥))   )
13::	⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥)
14:12,13,?: e20 41054	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   ¬ 𝐵 ∈ 𝑥   )
15::	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵), 𝑥 = 𝐵   ▶   𝑥 = 𝐵   )
16:7,15,?: e23 41082	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵), 𝑥 = 𝐵   ▶   𝑦 ∈ 𝑥   )
17:6,16,?: e23 41082	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵), 𝑥 = 𝐵   ▶   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)   )
18:17:	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   (𝑥 = 𝐵 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥))   )
19::	⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)
20:18,19,?: e20 41054	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   ¬ 𝑥 = 𝐵   )
21:3,?: e1a 40954	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
22:21,9,4,?: e121 40983	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   [𝑥 / 𝑥][𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
23:22,?: e2 40958	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   [𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
24:4,23,?: e12 41051	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   (𝑥 ∈ 𝐵 ∨ 𝐵 ∈ 𝑥 ∨ 𝑥 = 𝐵)   )
25:14,20,24,?: e222 40963	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑥 ∈ 𝐵   )
26:25:	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵)   )
27::	⊢ (∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑦∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
28:27,?: e0a 41099	⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → ∀𝑦(Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴))
29:28,26:	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)    ▶   ∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵)   )
30::	⊢ (∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑥∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
31:30,?: e0a 41099	⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → ∀𝑥(Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴))
32:31,29:	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑥 ∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵)   )
33:32,?: e1a 40954	⊢ (   (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 3220	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑥∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
2		alrim3con13v 40860	. . . . 5 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑥∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)) → ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → ∀𝑥(Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)))
3	1, 2	e0a 41099	. . . 4 ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → ∀𝑥(Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴))
4		ax-5 1907	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 → ∀𝑦 𝑥 ∈ 𝐴)
5		hbra1 3220	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑦∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
6	4, 5	hbral 3221	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑦∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
7		alrim3con13v 40860	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑦∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)) → ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → ∀𝑦(Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)))
8	6, 7	e0a 41099	. . . . 5 ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → ∀𝑦(Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴))
9		idn2 40940	. . . . . . . . . . 11 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   )
10		simpl 485	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝑦)
11	9, 10	e2 40958	. . . . . . . . . 10 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑥 ∈ 𝑦   )
12		simpr 487	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵)
13	9, 12	e2 40958	. . . . . . . . . 10 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑦 ∈ 𝐵   )
14		idn3 40942	. . . . . . . . . 10 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ,   𝐵 ∈ 𝑥   ▶   𝐵 ∈ 𝑥   )
15		pm3.2an3 1336	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝑦 → (𝑦 ∈ 𝐵 → (𝐵 ∈ 𝑥 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥))))
16	11, 13, 14, 15	e223 40962	. . . . . . . . 9 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ,   𝐵 ∈ 𝑥   ▶   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥)   )
17	16	in3 40936	. . . . . . . 8 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   (𝐵 ∈ 𝑥 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥))   )
18		en3lp 9071	. . . . . . . 8 ⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥)
19		con3 156	. . . . . . . 8 ⊢ ((𝐵 ∈ 𝑥 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥)) → (¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥) → ¬ 𝐵 ∈ 𝑥))
20	17, 18, 19	e20 41054	. . . . . . 7 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶    ¬ 𝐵 ∈ 𝑥   )
21		idn3 40942	. . . . . . . . . . 11 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ,   𝑥 = 𝐵   ▶   𝑥 = 𝐵   )
22		eleq2 2901	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐵 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝐵))
23	22	biimprcd 252	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝐵 → (𝑥 = 𝐵 → 𝑦 ∈ 𝑥))
24	13, 21, 23	e23 41082	. . . . . . . . . 10 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ,   𝑥 = 𝐵   ▶   𝑦 ∈ 𝑥   )
25		pm3.2 472	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝑦 → (𝑦 ∈ 𝑥 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)))
26	11, 24, 25	e23 41082	. . . . . . . . 9 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ,   𝑥 = 𝐵   ▶   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)   )
27	26	in3 40936	. . . . . . . 8 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   (𝑥 = 𝐵 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥))   )
28		en2lp 9063	. . . . . . . 8 ⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)
29		con3 156	. . . . . . . 8 ⊢ ((𝑥 = 𝐵 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) → (¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → ¬ 𝑥 = 𝐵))
30	27, 28, 29	e20 41054	. . . . . . 7 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶    ¬ 𝑥 = 𝐵   )
31		idn1 40901	. . . . . . . . 9 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   )
32		simp3 1134	. . . . . . . . 9 ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ 𝐴)
33	31, 32	e1a 40954	. . . . . . . 8 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   𝐵 ∈ 𝐴   )
34		simp2 1133	. . . . . . . . . . . 12 ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
35	31, 34	e1a 40954	. . . . . . . . . . 11 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
36		ralcom 3354	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
37	36	biimpi 218	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
38	35, 37	e1a 40954	. . . . . . . . . 10 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
39		simp1 1132	. . . . . . . . . . . 12 ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → Tr 𝐴)
40	31, 39	e1a 40954	. . . . . . . . . . 11 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   Tr 𝐴   )
41		trel 5171	. . . . . . . . . . . . 13 ⊢ (Tr 𝐴 → ((𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴) → 𝑦 ∈ 𝐴))
42	41	expd 418	. . . . . . . . . . . 12 ⊢ (Tr 𝐴 → (𝑦 ∈ 𝐵 → (𝐵 ∈ 𝐴 → 𝑦 ∈ 𝐴)))
43	40, 13, 33, 42	e121 40983	. . . . . . . . . . 11 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑦 ∈ 𝐴   )
44		trel 5171	. . . . . . . . . . . 12 ⊢ (Tr 𝐴 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴))
45	44	expd 418	. . . . . . . . . . 11 ⊢ (Tr 𝐴 → (𝑥 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑥 ∈ 𝐴)))
46	40, 11, 43, 45	e122 40980	. . . . . . . . . 10 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑥 ∈ 𝐴   )
47		rspsbc2 40861	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝐴 → (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → [𝑥 / 𝑥][𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))))
48	47	com13 88	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → (𝑥 ∈ 𝐴 → (𝐵 ∈ 𝐴 → [𝑥 / 𝑥][𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))))
49	38, 46, 33, 48	e121 40983	. . . . . . . . 9 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   [𝑥 / 𝑥][𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
50		equid 2015	. . . . . . . . . . 11 ⊢ 𝑥 = 𝑥
51		sbceq2a 3783	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑥 → ([𝑥 / 𝑥][𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ↔ [𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)))
52	50, 51	ax-mp 5	. . . . . . . . . 10 ⊢ ([𝑥 / 𝑥][𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ↔ [𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
53	52	biimpi 218	. . . . . . . . 9 ⊢ ([𝑥 / 𝑥][𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → [𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
54	49, 53	e2 40958	. . . . . . . 8 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   [𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
55		sbcoreleleq 40862	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝐴 → ([𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ↔ (𝑥 ∈ 𝐵 ∨ 𝐵 ∈ 𝑥 ∨ 𝑥 = 𝐵)))
56	55	biimpd 231	. . . . . . . 8 ⊢ (𝐵 ∈ 𝐴 → ([𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → (𝑥 ∈ 𝐵 ∨ 𝐵 ∈ 𝑥 ∨ 𝑥 = 𝐵)))
57	33, 54, 56	e12 41051	. . . . . . 7 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   (𝑥 ∈ 𝐵 ∨ 𝐵 ∈ 𝑥 ∨ 𝑥 = 𝐵)   )
58		3ornot23 40836	. . . . . . . 8 ⊢ ((¬ 𝐵 ∈ 𝑥 ∧ ¬ 𝑥 = 𝐵) → ((𝑥 ∈ 𝐵 ∨ 𝐵 ∈ 𝑥 ∨ 𝑥 = 𝐵) → 𝑥 ∈ 𝐵))
59	58	ex 415	. . . . . . 7 ⊢ (¬ 𝐵 ∈ 𝑥 → (¬ 𝑥 = 𝐵 → ((𝑥 ∈ 𝐵 ∨ 𝐵 ∈ 𝑥 ∨ 𝑥 = 𝐵) → 𝑥 ∈ 𝐵)))
60	20, 30, 57, 59	e222 40963	. . . . . 6 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑥 ∈ 𝐵   )
61	60	in2 40932	. . . . 5 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵)   )
62	8, 61	gen11nv 40944	. . . 4 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵)   )
63	3, 62	gen11nv 40944	. . 3 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵)   )
64		dftr2 5166	. . . 4 ⊢ (Tr 𝐵 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵))
65	64	biimpri 230	. . 3 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵) → Tr 𝐵)
66	63, 65	e1a 40954	. 2 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   Tr 𝐵   )
67	66	in1 40898	1 ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → Tr 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ w3o 1082   ∧ w3a 1083  ∀wal 1531   = wceq 1533   ∈ wcel 2110  ∀wral 3138  [wsbc 3771  Tr wtr 5164

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321  ax-un 7455  ax-reg 9050

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-br 5059  df-opab 5121  df-tr 5165  df-eprel 5459  df-fr 5508  df-vd1 40897  df-vd2 40905  df-vd3 40917

This theorem is referenced by: (None)