Theorem permaxext

Description: The Axiom of Extensionality ax-ext holds in permutation models. Part of Exercise II.9.2 of Kunen2 p. 148. (Contributed by Eric Schmidt, 6-Nov-2025)

	Ref	Expression
Hypotheses	permmodel.1	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}$$
	permmodel.2	$$⊢R=F^{-1}\circ \mathrm{E}$$
Assertion	permaxext	$$⊢\forall z\left(zRx\leftrightarrow zRy\right)\to x=y$$

Proof

Step	Hyp	Ref	Expression
1		permmodel.1	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}$$
2		permmodel.2	$$⊢R=F^{-1}\circ \mathrm{E}$$
3		vex	$$⊢z\in \mathrm{V}$$
4		vex	$$⊢x\in \mathrm{V}$$
5	1 2 3 4	brpermmodel	$$⊢zRx\leftrightarrow z\in F\left(x\right)$$
6		vex	$$⊢y\in \mathrm{V}$$
7	1 2 3 6	brpermmodel	$$⊢zRy\leftrightarrow z\in F\left(y\right)$$
8	5 7	bibi12i	$$⊢\left(zRx\leftrightarrow zRy\right)\leftrightarrow \left(z\in F\left(x\right)\leftrightarrow z\in F\left(y\right)\right)$$
9	8	albii	$$⊢\forall z\left(zRx\leftrightarrow zRy\right)\leftrightarrow \forall z\left(z\in F\left(x\right)\leftrightarrow z\in F\left(y\right)\right)$$
10		dfcleq	$$⊢F\left(x\right)=F\left(y\right)\leftrightarrow \forall z\left(z\in F\left(x\right)\leftrightarrow z\in F\left(y\right)\right)$$
11	9 10	bitr4i	$$⊢\forall z\left(zRx\leftrightarrow zRy\right)\leftrightarrow F\left(x\right)=F\left(y\right)$$
12		f1of1	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}\to F:\mathrm{V}\underset{1-1}{⟶}\mathrm{V}$$
13	1 12	ax-mp	$$⊢F:\mathrm{V}\underset{1-1}{⟶}\mathrm{V}$$
14		f1veqaeq	$$⊢\left(F:\mathrm{V}\underset{1-1}{⟶}\mathrm{V}\wedge \left(x\in \mathrm{V}\wedge y\in \mathrm{V}\right)\right)\to \left(F\left(x\right)=F\left(y\right)\to x=y\right)$$
15	13 14	mpan	$$⊢\left(x\in \mathrm{V}\wedge y\in \mathrm{V}\right)\to \left(F\left(x\right)=F\left(y\right)\to x=y\right)$$
16	15	el2v	$$⊢F\left(x\right)=F\left(y\right)\to x=y$$
17	11 16	sylbi	$$⊢\forall z\left(zRx\leftrightarrow zRy\right)\to x=y$$