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 \{⟨x, y⟩ \| φ\} [A] \leftrightarrow \exists x \in A [b/ y] φ$

Proof

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

Metamath Proof Explorer

Theorem isarep1

Proof