Theorem dffix2

Description: The fixpoints of a class in terms of its range. (Contributed by Scott Fenton, 16-Apr-2012)

	Ref	Expression
Assertion	dffix2	⊢ Fix 𝐴 = ran ( 𝐴 ∩ I )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2	1	elfix	⊢ ( 𝑥 ∈ Fix 𝐴 ↔ 𝑥 𝐴 𝑥 )
3	1	elrn	⊢ ( 𝑥 ∈ ran ( 𝐴 ∩ I ) ↔ ∃ 𝑦 𝑦 ( 𝐴 ∩ I ) 𝑥 )
4		brin	⊢ ( 𝑦 ( 𝐴 ∩ I ) 𝑥 ↔ ( 𝑦 𝐴 𝑥 ∧ 𝑦 I 𝑥 ) )
5		ancom	⊢ ( ( 𝑦 𝐴 𝑥 ∧ 𝑦 I 𝑥 ) ↔ ( 𝑦 I 𝑥 ∧ 𝑦 𝐴 𝑥 ) )
6	1	ideq	⊢ ( 𝑦 I 𝑥 ↔ 𝑦 = 𝑥 )
7	6	anbi1i	⊢ ( ( 𝑦 I 𝑥 ∧ 𝑦 𝐴 𝑥 ) ↔ ( 𝑦 = 𝑥 ∧ 𝑦 𝐴 𝑥 ) )
8	4 5 7	3bitri	⊢ ( 𝑦 ( 𝐴 ∩ I ) 𝑥 ↔ ( 𝑦 = 𝑥 ∧ 𝑦 𝐴 𝑥 ) )
9	8	exbii	⊢ ( ∃ 𝑦 𝑦 ( 𝐴 ∩ I ) 𝑥 ↔ ∃ 𝑦 ( 𝑦 = 𝑥 ∧ 𝑦 𝐴 𝑥 ) )
10		breq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 𝐴 𝑥 ↔ 𝑥 𝐴 𝑥 ) )
11	10	equsexvw	⊢ ( ∃ 𝑦 ( 𝑦 = 𝑥 ∧ 𝑦 𝐴 𝑥 ) ↔ 𝑥 𝐴 𝑥 )
12	3 9 11	3bitri	⊢ ( 𝑥 ∈ ran ( 𝐴 ∩ I ) ↔ 𝑥 𝐴 𝑥 )
13	2 12	bitr4i	⊢ ( 𝑥 ∈ Fix 𝐴 ↔ 𝑥 ∈ ran ( 𝐴 ∩ I ) )
14	13	eqriv	⊢ Fix 𝐴 = ran ( 𝐴 ∩ I )