Metamath Proof Explorer

Theorem dfcnvrefrel4

Description: Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-May-2024)

Ref Expression
Assertion dfcnvrefrel4 ⊢ CnvRefRel R ↔ R ⊆ I ∧ Rel ⁡ R

Proof

Step Hyp Ref Expression
1 df-cnvrefrel ⊢ CnvRefRel R ↔ R ∩ dom ⁡ R × ran ⁡ R ⊆ I ∩ dom ⁡ R × ran ⁡ R ∧ Rel ⁡ R
2 cnvref4 ⊢ Rel ⁡ R → R ∩ dom ⁡ R × ran ⁡ R ⊆ I ∩ dom ⁡ R × ran ⁡ R ↔ R ⊆ I
3 1 2 bianim ⊢ CnvRefRel R ↔ R ⊆ I ∧ Rel ⁡ R