This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )