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)

	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		opelopabsb	$$⊢⟨z,b⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}b/y\underset{\dot{}}{]}\phi$$
5		sbsbc	$$⊢\left[b/y\right]\phi \leftrightarrow \underset{\dot{}}{[}b/y\underset{\dot{}}{]}\phi$$
6	5	sbbii	$$⊢\left[z/x\right]\left[b/y\right]\phi \leftrightarrow \left[z/x\right]\underset{\dot{}}{[}b/y\underset{\dot{}}{]}\phi$$
7		sbsbc	$$⊢\left[z/x\right]\underset{\dot{}}{[}b/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}b/y\underset{\dot{}}{]}\phi$$
8	6 7	bitr2i	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}b/y\underset{\dot{}}{]}\phi \leftrightarrow \left[z/x\right]\left[b/y\right]\phi$$
9	3 4 8	3bitri	$$⊢z\left\{⟨x,y⟩|\phi \right\}b\leftrightarrow \left[z/x\right]\left[b/y\right]\phi$$
10	9	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$$
11		nfs1v	$$⊢Ⅎx\left[z/x\right]\left[b/y\right]\phi$$
12		nfv	$$⊢Ⅎz\left[b/y\right]\phi$$
13		sbequ12r	$$⊢z=x\to \left(\left[z/x\right]\left[b/y\right]\phi \leftrightarrow \left[b/y\right]\phi \right)$$
14	11 12 13	cbvrexw	$$⊢\exists z\in A\left[z/x\right]\left[b/y\right]\phi \leftrightarrow \exists x\in A\left[b/y\right]\phi$$
15	2 10 14	3bitri	$$⊢b\in \left\{⟨x,y⟩|\phi \right\}\left[A\right]\leftrightarrow \exists x\in A\left[b/y\right]\phi$$