Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
General auxiliary theorems (1)
Unordered and ordered pairs - extension for ordered pairs
or2expropbilem2
Next ⟩
or2expropbi
Metamath Proof Explorer
Ascii
Unicode
Theorem
or2expropbilem2
Description:
Lemma 2 for
or2expropbi
and
ich2exprop
.
(Contributed by
AV
, 16-Jul-2023)
Ref
Expression
Assertion
or2expropbilem2
⊢
∃
a
∃
b
A
B
=
a
b
∧
φ
↔
∃
x
∃
y
A
B
=
x
y
∧
[
˙
y
/
b
]
˙
[
˙
x
/
a
]
˙
φ
Proof
Step
Hyp
Ref
Expression
1
nfv
⊢
Ⅎ
x
A
B
=
a
b
∧
φ
2
nfv
⊢
Ⅎ
y
A
B
=
a
b
∧
φ
3
nfv
⊢
Ⅎ
a
A
B
=
x
y
4
nfcv
⊢
Ⅎ
_
a
y
5
nfsbc1v
⊢
Ⅎ
a
[
˙
x
/
a
]
˙
φ
6
4
5
nfsbcw
⊢
Ⅎ
a
[
˙
y
/
b
]
˙
[
˙
x
/
a
]
˙
φ
7
3
6
nfan
⊢
Ⅎ
a
A
B
=
x
y
∧
[
˙
y
/
b
]
˙
[
˙
x
/
a
]
˙
φ
8
nfv
⊢
Ⅎ
b
A
B
=
x
y
9
nfsbc1v
⊢
Ⅎ
b
[
˙
y
/
b
]
˙
[
˙
x
/
a
]
˙
φ
10
8
9
nfan
⊢
Ⅎ
b
A
B
=
x
y
∧
[
˙
y
/
b
]
˙
[
˙
x
/
a
]
˙
φ
11
opeq12
⊢
a
=
x
∧
b
=
y
→
a
b
=
x
y
12
11
eqeq2d
⊢
a
=
x
∧
b
=
y
→
A
B
=
a
b
↔
A
B
=
x
y
13
sbceq1a
⊢
a
=
x
→
φ
↔
[
˙
x
/
a
]
˙
φ
14
sbceq1a
⊢
b
=
y
→
[
˙
x
/
a
]
˙
φ
↔
[
˙
y
/
b
]
˙
[
˙
x
/
a
]
˙
φ
15
13
14
sylan9bb
⊢
a
=
x
∧
b
=
y
→
φ
↔
[
˙
y
/
b
]
˙
[
˙
x
/
a
]
˙
φ
16
12
15
anbi12d
⊢
a
=
x
∧
b
=
y
→
A
B
=
a
b
∧
φ
↔
A
B
=
x
y
∧
[
˙
y
/
b
]
˙
[
˙
x
/
a
]
˙
φ
17
1
2
7
10
16
cbvex2v
⊢
∃
a
∃
b
A
B
=
a
b
∧
φ
↔
∃
x
∃
y
A
B
=
x
y
∧
[
˙
y
/
b
]
˙
[
˙
x
/
a
]
˙
φ