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