Theorem tfrlem5 8365

Description: Lemma for transfinite recursion. The values of two acceptable functions are the same within their domains. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 24-May-2019.)

Hypothesis

Ref	Expression
tfrlem.1	⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}

Assertion

Ref	Expression
tfrlem5	⊢ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣))

Distinct variable groups:   𝑓,𝑔,𝑥,𝑦,ℎ,𝑢,𝑣,𝐹   𝐴,𝑔,ℎ

Allowed substitution hints:   𝐴(𝑥,𝑦,𝑣,𝑢,𝑓)

Proof of Theorem tfrlem5

Dummy variables 𝑧 𝑎 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tfrlem.1	. . 3 ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
2		vex 3467	. . 3 ⊢ 𝑔 ∈ V
3	1, 2	tfrlem3a 8362	. 2 ⊢ (𝑔 ∈ 𝐴 ↔ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))))
4		vex 3467	. . 3 ⊢ ℎ ∈ V
5	1, 4	tfrlem3a 8362	. 2 ⊢ (ℎ ∈ 𝐴 ↔ ∃𝑤 ∈ On (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎))))
6		reeanv 3243	. . 3 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ↔ (∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ ∃𝑤 ∈ On (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))))
7		fveq2 6882	. . . . . . . 8 ⊢ (𝑎 = 𝑥 → (𝑔‘𝑎) = (𝑔‘𝑥))
8		fveq2 6882	. . . . . . . 8 ⊢ (𝑎 = 𝑥 → (ℎ‘𝑎) = (ℎ‘𝑥))
9	7, 8	eqeq12d 2785	. . . . . . 7 ⊢ (𝑎 = 𝑥 → ((𝑔‘𝑎) = (ℎ‘𝑎) ↔ (𝑔‘𝑥) = (ℎ‘𝑥)))
10		onin 6393	. . . . . . . . 9 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 ∩ 𝑤) ∈ On)
11	10	3ad2ant1 1149	. . . . . . . 8 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (𝑧 ∩ 𝑤) ∈ On)
12		simp2ll 1257	. . . . . . . . . 10 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑔 Fn 𝑧)
13		fnfun 6636	. . . . . . . . . 10 ⊢ (𝑔 Fn 𝑧 → Fun 𝑔)
14	12, 13	syl 18	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → Fun 𝑔)
15		inss1 4197	. . . . . . . . . 10 ⊢ (𝑧 ∩ 𝑤) ⊆ 𝑧
16	12	fndmd 6641	. . . . . . . . . 10 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → dom 𝑔 = 𝑧)
17	15, 16	sseqtrrid 3988	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (𝑧 ∩ 𝑤) ⊆ dom 𝑔)
18	14, 17	jca 520	. . . . . . . 8 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (Fun 𝑔 ∧ (𝑧 ∩ 𝑤) ⊆ dom 𝑔))
19		simp2rl 1259	. . . . . . . . . 10 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ℎ Fn 𝑤)
20		fnfun 6636	. . . . . . . . . 10 ⊢ (ℎ Fn 𝑤 → Fun ℎ)
21	19, 20	syl 18	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → Fun ℎ)
22		inss2 4198	. . . . . . . . . 10 ⊢ (𝑧 ∩ 𝑤) ⊆ 𝑤
23	19	fndmd 6641	. . . . . . . . . 10 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → dom ℎ = 𝑤)
24	22, 23	sseqtrrid 3988	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (𝑧 ∩ 𝑤) ⊆ dom ℎ)
25	21, 24	jca 520	. . . . . . . 8 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (Fun ℎ ∧ (𝑧 ∩ 𝑤) ⊆ dom ℎ))
26		simp2lr 1258	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎)))
27		ssralv 4014	. . . . . . . . 9 ⊢ ((𝑧 ∩ 𝑤) ⊆ 𝑧 → (∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎)) → ∀𝑎 ∈ (𝑧 ∩ 𝑤)(𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))))
28	15, 26, 27	mpsyl 69	. . . . . . . 8 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ∀𝑎 ∈ (𝑧 ∩ 𝑤)(𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎)))
29		simp2rr 1260	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))
30		ssralv 4014	. . . . . . . . 9 ⊢ ((𝑧 ∩ 𝑤) ⊆ 𝑤 → (∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)) → ∀𝑎 ∈ (𝑧 ∩ 𝑤)(ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎))))
31	22, 29, 30	mpsyl 69	. . . . . . . 8 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ∀𝑎 ∈ (𝑧 ∩ 𝑤)(ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))
32	11, 18, 25, 28, 31	tfrlem1 8361	. . . . . . 7 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ∀𝑎 ∈ (𝑧 ∩ 𝑤)(𝑔‘𝑎) = (ℎ‘𝑎))
33		simp3l 1218	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑥𝑔𝑢)
34		fnbr 6644	. . . . . . . . 9 ⊢ ((𝑔 Fn 𝑧 ∧ 𝑥𝑔𝑢) → 𝑥 ∈ 𝑧)
35	12, 33, 34	syl2anc 595	. . . . . . . 8 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑥 ∈ 𝑧)
36		simp3r 1219	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑥ℎ𝑣)
37		fnbr 6644	. . . . . . . . 9 ⊢ ((ℎ Fn 𝑤 ∧ 𝑥ℎ𝑣) → 𝑥 ∈ 𝑤)
38	19, 36, 37	syl2anc 595	. . . . . . . 8 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑥 ∈ 𝑤)
39	35, 38	elind 4161	. . . . . . 7 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑥 ∈ (𝑧 ∩ 𝑤))
40	9, 32, 39	rspcdva 3591	. . . . . 6 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (𝑔‘𝑥) = (ℎ‘𝑥))
41		funbrfv 6930	. . . . . . 7 ⊢ (Fun 𝑔 → (𝑥𝑔𝑢 → (𝑔‘𝑥) = 𝑢))
42	14, 33, 41	sylc 66	. . . . . 6 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (𝑔‘𝑥) = 𝑢)
43		funbrfv 6930	. . . . . . 7 ⊢ (Fun ℎ → (𝑥ℎ𝑣 → (ℎ‘𝑥) = 𝑣))
44	21, 36, 43	sylc 66	. . . . . 6 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (ℎ‘𝑥) = 𝑣)
45	40, 42, 44	3eqtr3d 2812	. . . . 5 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑢 = 𝑣)
46	45	3exp 1135	. . . 4 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)))
47	46	rexlimivv 3213	. . 3 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣))
48	6, 47	sylbir 238	. 2 ⊢ ((∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ ∃𝑤 ∈ On (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣))
49	3, 5, 48	syl2anb 609	1 ⊢ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣))

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149  {cab 2747  ∀wral 3085  ∃wrex 3095   ∩ cin 3912   ⊆ wss 3913   class class class wbr 5113  dom cdm 5662   ↾ cres 5664  Oncon0 6361  Fun wfun 6531   Fn wfn 6532  ‘cfv 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-ord 6364  df-on 6365  df-iota 6493  df-fun 6539  df-fn 6540  df-fv 6545

This theorem is referenced by:  tfrlem7  8369