Theorem dfcnvrefrel3

Description: Alternate definition of the converse reflexive relation predicate. A relation is converse reflexive iff: for all elements on its domain and range, if for an element of its domain and for an element of its range there is the relation between them, then the two elements are the same, cf. the comment of dfrefrel3 . (Contributed by Peter Mazsa, 25-Jul-2021)

	Ref	Expression
Assertion	dfcnvrefrel3	⊢ ( CnvRefRel 𝑅 ↔ ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 𝑅 𝑦 → 𝑥 = 𝑦 ) ∧ Rel 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		df-cnvrefrel	⊢ ( CnvRefRel 𝑅 ↔ ( ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ∧ Rel 𝑅 ) )
2		inxpssidinxp	⊢ ( ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ↔ ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 𝑅 𝑦 → 𝑥 = 𝑦 ) )
3	2	anbi1i	⊢ ( ( ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ∧ Rel 𝑅 ) ↔ ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 𝑅 𝑦 → 𝑥 = 𝑦 ) ∧ Rel 𝑅 ) )
4	1 3	bitri	⊢ ( CnvRefRel 𝑅 ↔ ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 𝑅 𝑦 → 𝑥 = 𝑦 ) ∧ Rel 𝑅 ) )