Metamath Proof Explorer


Theorem brcici

Description: Prove that two objects are isomorphic by an explicit isomorphism. (Contributed by AV, 4-Apr-2020)

Ref Expression
Hypotheses cic.i I=IsoC
cic.b B=BaseC
cic.c φCCat
cic.x φXB
cic.y φYB
cic.f φFXIY
Assertion brcici φX𝑐CY

Proof

Step Hyp Ref Expression
1 cic.i I=IsoC
2 cic.b B=BaseC
3 cic.c φCCat
4 cic.x φXB
5 cic.y φYB
6 cic.f φFXIY
7 eleq1 f=FfXIYFXIY
8 7 spcegv FXIYFXIYffXIY
9 6 6 8 sylc φffXIY
10 1 2 3 4 5 cic φX𝑐CYffXIY
11 9 10 mpbird φX𝑐CY