Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Set theory
Removing some axiom requirements and disjoint variable conditions
bj-rabeqbid
Metamath Proof Explorer
Description: Version of rabeqbidv with two disjoint variable conditions removed and
the third replaced by a nonfreeness hypothesis. (Contributed by BJ , 27-Apr-2019)
Ref
Expression
Hypotheses
bj-rabeqbid.nf
⊢ Ⅎ x φ
bj-rabeqbid.1
⊢ φ → A = B
bj-rabeqbid.2
⊢ φ → ψ ↔ χ
Assertion
bj-rabeqbid
⊢ φ → x ∈ A | ψ = x ∈ B | χ
Proof
Step
Hyp
Ref
Expression
1
bj-rabeqbid.nf
⊢ Ⅎ x φ
2
bj-rabeqbid.1
⊢ φ → A = B
3
bj-rabeqbid.2
⊢ φ → ψ ↔ χ
4
1 2
bj-rabeqd
⊢ φ → x ∈ A | ψ = x ∈ B | ψ
5
1 3
rabbid
⊢ φ → x ∈ B | ψ = x ∈ B | χ
6
4 5
eqtrd
⊢ φ → x ∈ A | ψ = x ∈ B | χ