Theorem ifr0

Description: A class that is founded by the identity relation is null. (Contributed by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Assertion	ifr0	⊢ ( I Fr 𝐴 ↔ 𝐴 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		equid	⊢ 𝑥 = 𝑥
2		vex	⊢ 𝑥 ∈ V
3	2	ideq	⊢ ( 𝑥 I 𝑥 ↔ 𝑥 = 𝑥 )
4	1 3	mpbir	⊢ 𝑥 I 𝑥
5		frirr	⊢ ( ( I Fr 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 I 𝑥 )
6	5	ex	⊢ ( I Fr 𝐴 → ( 𝑥 ∈ 𝐴 → ¬ 𝑥 I 𝑥 ) )
7	4 6	mt2i	⊢ ( I Fr 𝐴 → ¬ 𝑥 ∈ 𝐴 )
8	7	eq0rdv	⊢ ( I Fr 𝐴 → 𝐴 = ∅ )
9		fr0	⊢ I Fr ∅
10		freq2	⊢ ( 𝐴 = ∅ → ( I Fr 𝐴 ↔ I Fr ∅ ) )
11	9 10	mpbiri	⊢ ( 𝐴 = ∅ → I Fr 𝐴 )
12	8 11	impbii	⊢ ( I Fr 𝐴 ↔ 𝐴 = ∅ )