Metamath Proof Explorer


Theorem f1oabexg

Description: The class of all 1-1-onto functions mapping one set to another is a set. (Contributed by Paul Chapman, 25-Feb-2008) (Proof shortened by AV, 9-Jun-2025)

Ref Expression
Hypothesis f1oabexg.1 F = f | f : A 1-1 onto B φ
Assertion f1oabexg A C B D F V

Proof

Step Hyp Ref Expression
1 f1oabexg.1 F = f | f : A 1-1 onto B φ
2 elex A C A V
3 elex B D B V
4 f1of f : A 1-1 onto B f : A B
5 4 ad2antrl A V B V f : A 1-1 onto B φ f : A B
6 simpl A V B V A V
7 simpr A V B V B V
8 5 6 7 fabexd A V B V f | f : A 1-1 onto B φ V
9 1 8 eqeltrid A V B V F V
10 2 3 9 syl2an A C B D F V