Metamath Proof Explorer


Theorem en2prd

Description: Two unordered pairs are equinumerous. (Contributed by BTernaryTau, 23-Dec-2024)

Ref Expression
Hypotheses en2prd.1 φ A V
en2prd.2 φ B W
en2prd.3 φ C X
en2prd.4 φ D Y
en2prd.5 φ A B
en2prd.6 φ C D
Assertion en2prd φ A B C D

Proof

Step Hyp Ref Expression
1 en2prd.1 φ A V
2 en2prd.2 φ B W
3 en2prd.3 φ C X
4 en2prd.4 φ D Y
5 en2prd.5 φ A B
6 en2prd.6 φ C D
7 prex A C B D V
8 f1oprg A V C X B W D Y A B C D A C B D : A B 1-1 onto C D
9 1 3 2 4 8 syl22anc φ A B C D A C B D : A B 1-1 onto C D
10 5 6 9 mp2and φ A C B D : A B 1-1 onto C D
11 f1oeq1 f = A C B D f : A B 1-1 onto C D A C B D : A B 1-1 onto C D
12 11 spcegv A C B D V A C B D : A B 1-1 onto C D f f : A B 1-1 onto C D
13 7 10 12 mpsyl φ f f : A B 1-1 onto C D
14 prex A B V
15 prex C D V
16 breng A B V C D V A B C D f f : A B 1-1 onto C D
17 14 15 16 mp2an A B C D f f : A B 1-1 onto C D
18 13 17 sylibr φ A B C D