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 𝑅 ↔ 𝐴 𝑅 𝐴 )