Metamath Proof Explorer


Theorem foelrnf

Description: Property of a surjective function. As foelrn but with less disjoint vars constraints. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypothesis foelrnf.1 _xF
Assertion foelrnf F:AontoBCBxAC=Fx

Proof

Step Hyp Ref Expression
1 foelrnf.1 _xF
2 1 dffo3f F:AontoBF:AByBxAy=Fx
3 2 simprbi F:AontoByBxAy=Fx
4 eqeq1 y=Cy=FxC=Fx
5 4 rexbidv y=CxAy=FxxAC=Fx
6 5 rspccva yBxAy=FxCBxAC=Fx
7 3 6 sylan F:AontoBCBxAC=Fx