Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Utility theorems
19.8aw
Next ⟩
19.9dev
Metamath Proof Explorer
Ascii
Unicode
Theorem
19.8aw
Description:
This is to
19.8a
what
spw
is to
sp
.
(Contributed by
SN
, 26-Sep-2024)
Ref
Expression
Hypothesis
19.8aw.1
⊢
x
=
y
→
φ
↔
ψ
Assertion
19.8aw
⊢
φ
→
∃
x
φ
Proof
Step
Hyp
Ref
Expression
1
19.8aw.1
⊢
x
=
y
→
φ
↔
ψ
2
alnex
⊢
∀
x
¬
φ
↔
¬
∃
x
φ
3
1
notbid
⊢
x
=
y
→
¬
φ
↔
¬
ψ
4
3
spw
⊢
∀
x
¬
φ
→
¬
φ
5
2
4
sylbir
⊢
¬
∃
x
φ
→
¬
φ
6
5
con4i
⊢
φ
→
∃
x
φ