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	⊢ 𝐹 : V –1-1-onto→ V
	permmodel.2	⊢ 𝑅 = ( ◡ 𝐹 ∘ E )
	brpermmodel.3	⊢ 𝐴 ∈ V
	brpermmodel.4	⊢ 𝐵 ∈ V
Assertion	brpermmodelcnv	⊢ ( 𝐴 𝑅 ( ◡ 𝐹 ‘ 𝐵 ) ↔ 𝐴 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		permmodel.1	⊢ 𝐹 : V –1-1-onto→ V
2		permmodel.2	⊢ 𝑅 = ( ◡ 𝐹 ∘ E )
3		brpermmodel.3	⊢ 𝐴 ∈ V
4		brpermmodel.4	⊢ 𝐵 ∈ V
5		fvex	⊢ ( ◡ 𝐹 ‘ 𝐵 ) ∈ V
6	1 2 3 5	brpermmodel	⊢ ( 𝐴 𝑅 ( ◡ 𝐹 ‘ 𝐵 ) ↔ 𝐴 ∈ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝐵 ) ) )
7		f1ocnvfv2	⊢ ( ( 𝐹 : V –1-1-onto→ V ∧ 𝐵 ∈ V ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝐵 ) ) = 𝐵 )
8	1 4 7	mp2an	⊢ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝐵 ) ) = 𝐵
9	8	eleq2i	⊢ ( 𝐴 ∈ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝐵 ) ) ↔ 𝐴 ∈ 𝐵 )
10	6 9	bitri	⊢ ( 𝐴 𝑅 ( ◡ 𝐹 ‘ 𝐵 ) ↔ 𝐴 ∈ 𝐵 )