Theorem brpermmodelcnv

Description: Ordinary membership expressed in terms of the permutation model's membership relation. (Contributed by Eric Schmidt, 6-Nov-2025)

	Ref	Expression
Hypotheses	permmodel.1	|- F : _V -1-1-onto-> _V
	permmodel.2	|- R = ( `' F o. _E )
	brpermmodel.3	|- A e. _V
	brpermmodel.4	|- B e. _V
Assertion	brpermmodelcnv	|- ( A R ( `' F ` B ) <-> A e. B )

Proof

Step	Hyp	Ref	Expression
1		permmodel.1	|- F : _V -1-1-onto-> _V
2		permmodel.2	|- R = ( `' F o. _E )
3		brpermmodel.3	|- A e. _V
4		brpermmodel.4	|- B e. _V
5		fvex	|- ( `' F ` B ) e. _V
6	1 2 3 5	brpermmodel	|- ( A R ( `' F ` B ) <-> A e. ( F ` ( `' F ` B ) ) )
7		f1ocnvfv2	|- ( ( F : _V -1-1-onto-> _V /\ B e. _V ) -> ( F ` ( `' F ` B ) ) = B )
8	1 4 7	mp2an	|- ( F ` ( `' F ` B ) ) = B
9	8	eleq2i	|- ( A e. ( F ` ( `' F ` B ) ) <-> A e. B )
10	6 9	bitri	|- ( A R ( `' F ` B ) <-> A e. B )