Description: Version of rabbidva2 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | bj-rabbida2.nf | ⊢ Ⅎ 𝑥 𝜑 | |
bj-rabbida2.1 | ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝜒 ) ) ) | ||
Assertion | bj-rabbida2 | ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝑥 ∈ 𝐵 ∣ 𝜒 } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-rabbida2.nf | ⊢ Ⅎ 𝑥 𝜑 | |
2 | bj-rabbida2.1 | ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝜒 ) ) ) | |
3 | 1 2 | abbid | ⊢ ( 𝜑 → { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜒 ) } ) |
4 | df-rab | ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } | |
5 | df-rab | ⊢ { 𝑥 ∈ 𝐵 ∣ 𝜒 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜒 ) } | |
6 | 3 4 5 | 3eqtr4g | ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝑥 ∈ 𝐵 ∣ 𝜒 } ) |