Theorem tratrbVD 44881

Description: Virtual deduction proof of tratrb 44556. 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 44647	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   Tr 𝐴   )
3:1,?: e1a 44647	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)    ▶   ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
4:1,?: e1a 44647	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   𝐵 ∈ 𝐴   )
5::	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   )
6:5,?: e2 44651	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑥 ∈ 𝑦   )
7:5,?: e2 44651	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑦 ∈ 𝐵   )
8:2,7,4,?: e121 44676	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑦 ∈ 𝐴   )
9:2,6,8,?: e122 44673	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑥 ∈ 𝐴   )
10::	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵), 𝐵 ∈ 𝑥   ▶   𝐵 ∈ 𝑥   )
11:6,7,10,?: e223 44655	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵), 𝐵 ∈ 𝑥   ▶   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥)   )
12:11:	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   (𝐵 ∈ 𝑥 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥))   )
13::	⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥)
14:12,13,?: e20 44747	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   ¬ 𝐵 ∈ 𝑥   )
15::	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵), 𝑥 = 𝐵   ▶   𝑥 = 𝐵   )
16:7,15,?: e23 44775	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵), 𝑥 = 𝐵   ▶   𝑦 ∈ 𝑥   )
17:6,16,?: e23 44775	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵), 𝑥 = 𝐵   ▶   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)   )
18:17:	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   (𝑥 = 𝐵 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥))   )
19::	⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)
20:18,19,?: e20 44747	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   ¬ 𝑥 = 𝐵   )
21:3,?: e1a 44647	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
22:21,9,4,?: e121 44676	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   [𝑥 / 𝑥][𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
23:22,?: e2 44651	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   [𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
24:4,23,?: e12 44744	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   (𝑥 ∈ 𝐵 ∨ 𝐵 ∈ 𝑥 ∨ 𝑥 = 𝐵)   )
25:14,20,24,?: e222 44656	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴), (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑥 ∈ 𝐵   )
26:25:	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵)   )
27::	⊢ (∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑦∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
28:27,?: e0a 44792	⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → ∀𝑦(Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴))
29:28,26:	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)    ▶   ∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵)   )
30::	⊢ (∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑥∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
31:30,?: e0a 44792	⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → ∀𝑥(Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴))
32:31,29:	⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴(𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑥 ∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵)   )
33:32,?: e1a 44647	⊢ (   (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 3301	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑥∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
2		alrim3con13v 44553	. . . . 5 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑥∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)) → ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → ∀𝑥(Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)))
3	1, 2	e0a 44792	. . . 4 ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → ∀𝑥(Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴))
4		ax-5 1910	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 → ∀𝑦 𝑥 ∈ 𝐴)
5		hbra1 3301	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑦∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
6	4, 5	hbral 3308	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑦∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
7		alrim3con13v 44553	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑦∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)) → ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → ∀𝑦(Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)))
8	6, 7	e0a 44792	. . . . 5 ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → ∀𝑦(Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴))
9		idn2 44633	. . . . . . . . . . 11 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   )
10		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝑦)
11	9, 10	e2 44651	. . . . . . . . . 10 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑥 ∈ 𝑦   )
12		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵)
13	9, 12	e2 44651	. . . . . . . . . 10 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑦 ∈ 𝐵   )
14		idn3 44635	. . . . . . . . . 10 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ,   𝐵 ∈ 𝑥   ▶   𝐵 ∈ 𝑥   )
15		pm3.2an3 1341	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝑦 → (𝑦 ∈ 𝐵 → (𝐵 ∈ 𝑥 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥))))
16	11, 13, 14, 15	e223 44655	. . . . . . . . 9 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ,   𝐵 ∈ 𝑥   ▶   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥)   )
17	16	in3 44629	. . . . . . . 8 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   (𝐵 ∈ 𝑥 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥))   )
18		en3lp 9654	. . . . . . . 8 ⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥)
19		con3 153	. . . . . . . 8 ⊢ ((𝐵 ∈ 𝑥 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥)) → (¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥) → ¬ 𝐵 ∈ 𝑥))
20	17, 18, 19	e20 44747	. . . . . . 7 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶    ¬ 𝐵 ∈ 𝑥   )
21		idn3 44635	. . . . . . . . . . 11 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ,   𝑥 = 𝐵   ▶   𝑥 = 𝐵   )
22		eleq2 2830	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐵 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝐵))
23	22	biimprcd 250	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝐵 → (𝑥 = 𝐵 → 𝑦 ∈ 𝑥))
24	13, 21, 23	e23 44775	. . . . . . . . . 10 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ,   𝑥 = 𝐵   ▶   𝑦 ∈ 𝑥   )
25		pm3.2 469	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝑦 → (𝑦 ∈ 𝑥 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)))
26	11, 24, 25	e23 44775	. . . . . . . . 9 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ,   𝑥 = 𝐵   ▶   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)   )
27	26	in3 44629	. . . . . . . 8 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   (𝑥 = 𝐵 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥))   )
28		en2lp 9646	. . . . . . . 8 ⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)
29		con3 153	. . . . . . . 8 ⊢ ((𝑥 = 𝐵 → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) → (¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → ¬ 𝑥 = 𝐵))
30	27, 28, 29	e20 44747	. . . . . . 7 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶    ¬ 𝑥 = 𝐵   )
31		idn1 44594	. . . . . . . . 9 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   )
32		simp3 1139	. . . . . . . . 9 ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ 𝐴)
33	31, 32	e1a 44647	. . . . . . . 8 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   𝐵 ∈ 𝐴   )
34		simp2 1138	. . . . . . . . . . . 12 ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
35	31, 34	e1a 44647	. . . . . . . . . . 11 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
36		ralcom 3289	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
37	36	biimpi 216	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
38	35, 37	e1a 44647	. . . . . . . . . 10 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
39		simp1 1137	. . . . . . . . . . . 12 ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → Tr 𝐴)
40	31, 39	e1a 44647	. . . . . . . . . . 11 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   Tr 𝐴   )
41		trel 5268	. . . . . . . . . . . . 13 ⊢ (Tr 𝐴 → ((𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴) → 𝑦 ∈ 𝐴))
42	41	expd 415	. . . . . . . . . . . 12 ⊢ (Tr 𝐴 → (𝑦 ∈ 𝐵 → (𝐵 ∈ 𝐴 → 𝑦 ∈ 𝐴)))
43	40, 13, 33, 42	e121 44676	. . . . . . . . . . 11 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑦 ∈ 𝐴   )
44		trel 5268	. . . . . . . . . . . 12 ⊢ (Tr 𝐴 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴))
45	44	expd 415	. . . . . . . . . . 11 ⊢ (Tr 𝐴 → (𝑥 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑥 ∈ 𝐴)))
46	40, 11, 43, 45	e122 44673	. . . . . . . . . 10 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑥 ∈ 𝐴   )
47		rspsbc2 44554	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝐴 → (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → [𝑥 / 𝑥][𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))))
48	47	com13 88	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → (𝑥 ∈ 𝐴 → (𝐵 ∈ 𝐴 → [𝑥 / 𝑥][𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))))
49	38, 46, 33, 48	e121 44676	. . . . . . . . 9 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   [𝑥 / 𝑥][𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
50		equid 2011	. . . . . . . . . . 11 ⊢ 𝑥 = 𝑥
51		sbceq2a 3800	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑥 → ([𝑥 / 𝑥][𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ↔ [𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)))
52	50, 51	ax-mp 5	. . . . . . . . . 10 ⊢ ([𝑥 / 𝑥][𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ↔ [𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
53	52	biimpi 216	. . . . . . . . 9 ⊢ ([𝑥 / 𝑥][𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → [𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
54	49, 53	e2 44651	. . . . . . . 8 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   [𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
55		sbcoreleleq 44555	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝐴 → ([𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ↔ (𝑥 ∈ 𝐵 ∨ 𝐵 ∈ 𝑥 ∨ 𝑥 = 𝐵)))
56	55	biimpd 229	. . . . . . . 8 ⊢ (𝐵 ∈ 𝐴 → ([𝐵 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → (𝑥 ∈ 𝐵 ∨ 𝐵 ∈ 𝑥 ∨ 𝑥 = 𝐵)))
57	33, 54, 56	e12 44744	. . . . . . 7 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   (𝑥 ∈ 𝐵 ∨ 𝐵 ∈ 𝑥 ∨ 𝑥 = 𝐵)   )
58		3ornot23 44529	. . . . . . . 8 ⊢ ((¬ 𝐵 ∈ 𝑥 ∧ ¬ 𝑥 = 𝐵) → ((𝑥 ∈ 𝐵 ∨ 𝐵 ∈ 𝑥 ∨ 𝑥 = 𝐵) → 𝑥 ∈ 𝐵))
59	58	ex 412	. . . . . . 7 ⊢ (¬ 𝐵 ∈ 𝑥 → (¬ 𝑥 = 𝐵 → ((𝑥 ∈ 𝐵 ∨ 𝐵 ∈ 𝑥 ∨ 𝑥 = 𝐵) → 𝑥 ∈ 𝐵)))
60	20, 30, 57, 59	e222 44656	. . . . . 6 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ,   (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)   ▶   𝑥 ∈ 𝐵   )
61	60	in2 44625	. . . . 5 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵)   )
62	8, 61	gen11nv 44637	. . . 4 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵)   )
63	3, 62	gen11nv 44637	. . 3 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵)   )
64		dftr2 5261	. . . 4 ⊢ (Tr 𝐵 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵))
65	64	biimpri 228	. . 3 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵) → Tr 𝐵)
66	63, 65	e1a 44647	. 2 ⊢ (   (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴)   ▶   Tr 𝐵   )
67	66	in1 44591	1 ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → Tr 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ w3o 1086   ∧ w3a 1087  ∀wal 1538   = wceq 1540   ∈ wcel 2108  ∀wral 3061  [wsbc 3788  Tr wtr 5259

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-reg 9632

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-tr 5260  df-eprel 5584  df-fr 5637  df-vd1 44590  df-vd2 44598  df-vd3 44610

This theorem is referenced by: (None)