Metamath Proof Explorer


Theorem f1dom2gOLD

Description: Obsolete version of f1dom2g as of 25-Sep-2024. (Contributed by Mario Carneiro, 24-Jun-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion f1dom2gOLD A V B W F : A 1-1 B A B

Proof

Step Hyp Ref Expression
1 f1f F : A 1-1 B F : A B
2 fex2 F : A B A V B W F V
3 1 2 syl3an1 F : A 1-1 B A V B W F V
4 3 3coml A V B W F : A 1-1 B F V
5 simp3 A V B W F : A 1-1 B F : A 1-1 B
6 f1eq1 f = F f : A 1-1 B F : A 1-1 B
7 4 5 6 spcedv A V B W F : A 1-1 B f f : A 1-1 B
8 brdomg B W A B f f : A 1-1 B
9 8 3ad2ant2 A V B W F : A 1-1 B A B f f : A 1-1 B
10 7 9 mpbird A V B W F : A 1-1 B A B