Metamath Proof Explorer


Theorem bnj1536

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1536.1 φ F Fn A
bnj1536.2 φ G Fn A
bnj1536.3 φ B A
bnj1536.4 φ x B F x = G x
Assertion bnj1536 φ F B = G B

Proof

Step Hyp Ref Expression
1 bnj1536.1 φ F Fn A
2 bnj1536.2 φ G Fn A
3 bnj1536.3 φ B A
4 bnj1536.4 φ x B F x = G x
5 fvreseq F Fn A G Fn A B A F B = G B x B F x = G x
6 1 2 3 5 syl21anc φ F B = G B x B F x = G x
7 4 6 mpbird φ F B = G B