Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Set theory
Classes without the axiom of extensionality
bj-ceqsalg
Metamath Proof Explorer
Description: Remove from ceqsalg dependency on ax-ext (and on df-cleq and
df-v ). See also bj-ceqsalgv . (Contributed by BJ , 12-Oct-2019)
(Proof modification is discouraged.)
Ref
Expression
Hypotheses
bj-ceqsalg.1
⊢ Ⅎ 𝑥 𝜓
bj-ceqsalg.2
⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion
bj-ceqsalg
⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ 𝜓 ) )
Proof
Step
Hyp
Ref
Expression
1
bj-ceqsalg.1
⊢ Ⅎ 𝑥 𝜓
2
bj-ceqsalg.2
⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
3
bj-elisset
⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 𝑥 = 𝐴 )
4
1 2
bj-ceqsalg0
⊢ ( ∃ 𝑥 𝑥 = 𝐴 → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ 𝜓 ) )
5
3 4
syl
⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ 𝜓 ) )