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

Metamath Proof Explorer

Theorem brfullfun

Description: A binary relation form condition for the full function. (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Hypotheses brfullfun.1 ⊢ A ∈ V
brfullfun.2 ⊢ B ∈ V
Assertion brfullfun ⊢ A 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F B ↔ B = F ⁡ A

Proof

Step Hyp Ref Expression
1 brfullfun.1 ⊢ A ∈ V
2 brfullfun.2 ⊢ B ∈ V
3 eqcom ⊢ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ⁡ A = B ↔ B = 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ⁡ A
4 fullfunfnv ⊢ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F Fn V
5 fnbrfvb ⊢ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F Fn V ∧ A ∈ V → 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ⁡ A = B ↔ A 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F B
6 4 1 5 mp2an ⊢ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ⁡ A = B ↔ A 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F B
7 fullfunfv ⊢ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ⁡ A = F ⁡ A
8 7 eqeq2i ⊢ B = 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ⁡ A ↔ B = F ⁡ A
9 3 6 8 3bitr3i ⊢ A 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F B ↔ B = F ⁡ A