Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
First-order logic
Adding ax-4
bj-2exbi
Next ⟩
bj-3exbi
Metamath Proof Explorer
Ascii
Unicode
Theorem
bj-2exbi
Description:
Closed form of
2exbii
.
(Contributed by
BJ
, 6-May-2019)
Ref
Expression
Assertion
bj-2exbi
⊢
∀
x
∀
y
φ
↔
ψ
→
∃
x
∃
y
φ
↔
∃
x
∃
y
ψ
Proof
Step
Hyp
Ref
Expression
1
exbi
⊢
∀
y
φ
↔
ψ
→
∃
y
φ
↔
∃
y
ψ
2
1
alexbii
⊢
∀
x
∀
y
φ
↔
ψ
→
∃
x
∃
y
φ
↔
∃
x
∃
y
ψ