This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem caofref

Description: Transfer a reflexive law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014)

Ref Expression
Hypotheses caofref.1 ⊢ φ → A ∈ V
caofref.2 ⊢ φ → F : A ⟶ S
caofref.3 ⊢ φ ∧ x ∈ S → x R x
Assertion caofref ⊢ φ → F R f F

Proof

Step Hyp Ref Expression
1 caofref.1 ⊢ φ → A ∈ V
2 caofref.2 ⊢ φ → F : A ⟶ S
3 caofref.3 ⊢ φ ∧ x ∈ S → x R x
4 id ⊢ x = F ⁡ w → x = F ⁡ w
5 4 4 breq12d ⊢ x = F ⁡ w → x R x ↔ F ⁡ w R F ⁡ w
6 3 ralrimiva ⊢ φ → ∀ x ∈ S x R x
7 6 adantr ⊢ φ ∧ w ∈ A → ∀ x ∈ S x R x
8 2 ffvelcdmda ⊢ φ ∧ w ∈ A → F ⁡ w ∈ S
9 5 7 8 rspcdva ⊢ φ ∧ w ∈ A → F ⁡ w R F ⁡ w
10 9 ralrimiva ⊢ φ → ∀ w ∈ A F ⁡ w R F ⁡ w
11 2 ffnd ⊢ φ → F Fn A
12 inidm ⊢ A ∩ A = A
13 eqidd ⊢ φ ∧ w ∈ A → F ⁡ w = F ⁡ w
14 11 11 1 1 12 13 13 ofrfval ⊢ φ → F R f F ↔ ∀ w ∈ A F ⁡ w R F ⁡ w
15 10 14 mpbird ⊢ φ → F R f F