Theorem raldifb

Description: Restricted universal quantification on a class difference in terms of an implication. (Contributed by Alexander van der Vekens, 3-Jan-2018)

	Ref	Expression
Assertion	raldifb	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∉ 𝐵 → 𝜑 ) ↔ ∀ 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		impexp	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∉ 𝐵 ) → 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∉ 𝐵 → 𝜑 ) ) )
2		df-nel	⊢ ( 𝑥 ∉ 𝐵 ↔ ¬ 𝑥 ∈ 𝐵 )
3	2	anbi2i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∉ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) )
4		eldif	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) )
5	3 4	bitr4i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∉ 𝐵 ) ↔ 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) )
6	5	imbi1i	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∉ 𝐵 ) → 𝜑 ) ↔ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → 𝜑 ) )
7	1 6	bitr3i	⊢ ( ( 𝑥 ∈ 𝐴 → ( 𝑥 ∉ 𝐵 → 𝜑 ) ) ↔ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → 𝜑 ) )
8	7	ralbii2	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∉ 𝐵 → 𝜑 ) ↔ ∀ 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝜑 )