Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
First-order logic
Adding ax-4
bj-hbyfrbi
Next ⟩
bj-exalim
Metamath Proof Explorer
Ascii
Unicode
Theorem
bj-hbyfrbi
Description:
Version of
bj-hbxfrbi
with existential quantifiers.
(Contributed by
BJ
, 23-Aug-2023)
Ref
Expression
Assertion
bj-hbyfrbi
⊢
φ
↔
ψ
∧
∀
x
φ
↔
ψ
→
∃
x
φ
→
φ
↔
∃
x
ψ
→
ψ
Proof
Step
Hyp
Ref
Expression
1
exbi
⊢
∀
x
φ
↔
ψ
→
∃
x
φ
↔
∃
x
ψ
2
1
adantl
⊢
φ
↔
ψ
∧
∀
x
φ
↔
ψ
→
∃
x
φ
↔
∃
x
ψ
3
simpl
⊢
φ
↔
ψ
∧
∀
x
φ
↔
ψ
→
φ
↔
ψ
4
2
3
imbi12d
⊢
φ
↔
ψ
∧
∀
x
φ
↔
ψ
→
∃
x
φ
→
φ
↔
∃
x
ψ
→
ψ