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 ⊢ A ∈ V
Assertion elfix ⊢ A ∈ 𝖥𝗂𝗑 R ↔ A R A

Proof

Step Hyp Ref Expression
1 elfix.1 ⊢ A ∈ V
2 df-fix ⊢ 𝖥𝗂𝗑 R = dom ⁡ R ∩ I
3 2 eleq2i ⊢ A ∈ 𝖥𝗂𝗑 R ↔ A ∈ dom ⁡ R ∩ I
4 1 eldm ⊢ A ∈ dom ⁡ R ∩ I ↔ ∃ x A R ∩ I x
5 brin ⊢ A R ∩ I x ↔ A R x ∧ A I x
6 ancom ⊢ A R x ∧ A I x ↔ A I x ∧ A R x
7 vex ⊢ x ∈ V
8 7 ideq ⊢ A I x ↔ A = x
9 eqcom ⊢ A = x ↔ x = A
10 8 9 bitri ⊢ A I x ↔ x = A
11 10 anbi1i ⊢ A I x ∧ A R x ↔ x = A ∧ A R x
12 5 6 11 3bitri ⊢ A R ∩ I x ↔ x = A ∧ A R x
13 12 exbii ⊢ ∃ x A R ∩ I x ↔ ∃ x x = A ∧ A R x
14 4 13 bitri ⊢ A ∈ dom ⁡ R ∩ I ↔ ∃ x x = A ∧ A R x
15 breq2 ⊢ x = A → A R x ↔ A R A
16 1 15 ceqsexv ⊢ ∃ x x = A ∧ A R x ↔ A R A
17 3 14 16 3bitri ⊢ A ∈ 𝖥𝗂𝗑 R ↔ A R A