Metamath Proof Explorer

Theorem dffun2OLD

Description: Obsolete version of dffun2 as of 29-Dec-2024. (Contributed by NM, 29-Dec-1996) Avoid ax-10 , ax-12 . (Revised by SN, 19-Dec-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion dffun2OLD ⊢ Fun ⁡ A ↔ Rel ⁡ A ∧ ∀ x ∀ y ∀ z x A y ∧ x A z → y = z

Proof

Step Hyp Ref Expression
1 df-fun ⊢ Fun ⁡ A ↔ Rel ⁡ A ∧ A ∘ A -1 ⊆ I
2 cotrg ⊢ A ∘ A -1 ⊆ I ↔ ∀ y ∀ x ∀ z y A -1 x ∧ x A z → y I z
3 alcom ⊢ ∀ y ∀ x ∀ z y A -1 x ∧ x A z → y I z ↔ ∀ x ∀ y ∀ z y A -1 x ∧ x A z → y I z
4 vex ⊢ y ∈ V
5 vex ⊢ x ∈ V
6 4 5 brcnv ⊢ y A -1 x ↔ x A y
7 6 anbi1i ⊢ y A -1 x ∧ x A z ↔ x A y ∧ x A z
8 vex ⊢ z ∈ V
9 8 ideq ⊢ y I z ↔ y = z
10 7 9 imbi12i ⊢ y A -1 x ∧ x A z → y I z ↔ x A y ∧ x A z → y = z
11 10 3albii ⊢ ∀ x ∀ y ∀ z y A -1 x ∧ x A z → y I z ↔ ∀ x ∀ y ∀ z x A y ∧ x A z → y = z
12 3 11 bitri ⊢ ∀ y ∀ x ∀ z y A -1 x ∧ x A z → y I z ↔ ∀ x ∀ y ∀ z x A y ∧ x A z → y = z
13 2 12 bitri ⊢ A ∘ A -1 ⊆ I ↔ ∀ x ∀ y ∀ z x A y ∧ x A z → y = z
14 13 anbi2i ⊢ Rel ⁡ A ∧ A ∘ A -1 ⊆ I ↔ Rel ⁡ A ∧ ∀ x ∀ y ∀ z x A y ∧ x A z → y = z
15 1 14 bitri ⊢ Fun ⁡ A ↔ Rel ⁡ A ∧ ∀ x ∀ y ∀ z x A y ∧ x A z → y = z