Theorem rabbida4

Description: Version of rabbidva2 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019)

	Ref	Expression
Hypotheses	rabbida4.nf	⊢ Ⅎ 𝑥 𝜑
	rabbida4.1	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝜒 ) ) )
Assertion	rabbida4	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝑥 ∈ 𝐵 ∣ 𝜒 } )

Proof

Step	Hyp	Ref	Expression
1		rabbida4.nf	⊢ Ⅎ 𝑥 𝜑
2		rabbida4.1	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝜒 ) ) )
3	1 2	abbid	⊢ ( 𝜑 → { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜒 ) } )
4		df-rab	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) }
5		df-rab	⊢ { 𝑥 ∈ 𝐵 ∣ 𝜒 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜒 ) }
6	3 4 5	3eqtr4g	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝑥 ∈ 𝐵 ∣ 𝜒 } )