Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Equinumerosity
en2prd
Next ⟩
enpr2d
Metamath Proof Explorer
Ascii
Unicode
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