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

Metamath Proof Explorer

Theorem elfix

Description: Membership in the fixpoints of a class. (Contributed by Scott Fenton, 11-Apr-2012)

Ref Expression
Hypothesis elfix.1 ⊢ 𝐴 ∈ V
Assertion elfix ( 𝐴 ∈ Fix 𝑅 ↔ 𝐴 𝑅 𝐴 )

Proof

Step Hyp Ref Expression
1 elfix.1 ⊢ 𝐴 ∈ V
2 df-fix ⊢ Fix 𝑅 = dom ( 𝑅 ∩ I )
3 2 eleq2i ⊢ ( 𝐴 ∈ Fix 𝑅 ↔ 𝐴 ∈ dom ( 𝑅 ∩ I ) )
4 1 eldm ⊢ ( 𝐴 ∈ dom ( 𝑅 ∩ I ) ↔ ∃ 𝑥 𝐴 ( 𝑅 ∩ I ) 𝑥 )
5 brin ⊢ ( 𝐴 ( 𝑅 ∩ I ) 𝑥 ↔ ( 𝐴 𝑅 𝑥 ∧ 𝐴 I 𝑥 ) )
6 ancom ⊢ ( ( 𝐴 𝑅 𝑥 ∧ 𝐴 I 𝑥 ) ↔ ( 𝐴 I 𝑥 ∧ 𝐴 𝑅 𝑥 ) )
7 vex ⊢ 𝑥 ∈ V
8 7 ideq ⊢ ( 𝐴 I 𝑥 ↔ 𝐴 = 𝑥 )
9 eqcom ⊢ ( 𝐴 = 𝑥 ↔ 𝑥 = 𝐴 )
10 8 9 bitri ⊢ ( 𝐴 I 𝑥 ↔ 𝑥 = 𝐴 )
11 10 anbi1i ⊢ ( ( 𝐴 I 𝑥 ∧ 𝐴 𝑅 𝑥 ) ↔ ( 𝑥 = 𝐴 ∧ 𝐴 𝑅 𝑥 ) )
12 5 6 11 3bitri ⊢ ( 𝐴 ( 𝑅 ∩ I ) 𝑥 ↔ ( 𝑥 = 𝐴 ∧ 𝐴 𝑅 𝑥 ) )
13 12 exbii ⊢ ( ∃ 𝑥 𝐴 ( 𝑅 ∩ I ) 𝑥 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝐴 𝑅 𝑥 ) )
14 4 13 bitri ⊢ ( 𝐴 ∈ dom ( 𝑅 ∩ I ) ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝐴 𝑅 𝑥 ) )
15 breq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐴 𝑅 𝑥 ↔ 𝐴 𝑅 𝐴 ) )
16 1 15 ceqsexv ⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝐴 𝑅 𝑥 ) ↔ 𝐴 𝑅 𝐴 )
17 3 14 16 3bitri ⊢ ( 𝐴 ∈ Fix 𝑅 ↔ 𝐴 𝑅 𝐴 )