Theorem isarep1

Description: Part of a study of the Axiom of Replacement used by the Isabelle prover. The object PrimReplace is apparently the image of the function encoded by ph ( x , y ) i.e. the class ( { <. x , y >. | ph } " A ) . If so, we can prove Isabelle's "Axiom of Replacement" conclusion without using the Axiom of Replacement, for which I (N. Megill) currently have no explanation. (Contributed by NM, 26-Oct-2006) (Proof shortened by Mario Carneiro, 4-Dec-2016) (Proof shortened by SN, 19-Dec-2024)

	Ref	Expression
Assertion	isarep1	$$⊢b\in \left\{⟨x,y⟩|\phi \right\}\left[A\right]\leftrightarrow \exists x\in A\left[b/y\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢b\in \mathrm{V}$$
2	1	elima	$$⊢b\in \left\{⟨x,y⟩|\phi \right\}\left[A\right]\leftrightarrow \exists z\in Az\left\{⟨x,y⟩|\phi \right\}b$$
3		df-br	$$⊢z\left\{⟨x,y⟩|\phi \right\}b\leftrightarrow ⟨z,b⟩\in \left\{⟨x,y⟩|\phi \right\}$$
4		vopelopabsb	$$⊢⟨z,b⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \left[z/x\right]\left[b/y\right]\phi$$
5	3 4	bitri	$$⊢z\left\{⟨x,y⟩|\phi \right\}b\leftrightarrow \left[z/x\right]\left[b/y\right]\phi$$
6	5	rexbii	$$⊢\exists z\in Az\left\{⟨x,y⟩|\phi \right\}b\leftrightarrow \exists z\in A\left[z/x\right]\left[b/y\right]\phi$$
7		nfs1v	$$⊢Ⅎx\left[z/x\right]\left[b/y\right]\phi$$
8		nfv	$$⊢Ⅎz\left[b/y\right]\phi$$
9		sbequ12r	$$⊢z=x\to \left(\left[z/x\right]\left[b/y\right]\phi \leftrightarrow \left[b/y\right]\phi \right)$$
10	7 8 9	cbvrexw	$$⊢\exists z\in A\left[z/x\right]\left[b/y\right]\phi \leftrightarrow \exists x\in A\left[b/y\right]\phi$$
11	2 6 10	3bitri	$$⊢b\in \left\{⟨x,y⟩|\phi \right\}\left[A\right]\leftrightarrow \exists x\in A\left[b/y\right]\phi$$