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	⊢ ( 𝑏 ∈ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } “ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 [ 𝑏 / 𝑦 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑏 ∈ V
2	1	elima	⊢ ( 𝑏 ∈ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } “ 𝐴 ) ↔ ∃ 𝑧 ∈ 𝐴 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑏 )
3		df-br	⊢ ( 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑏 ↔ ⟨ 𝑧 , 𝑏 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
4		vopelopabsb	⊢ ( ⟨ 𝑧 , 𝑏 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝑧 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 )
5	3 4	bitri	⊢ ( 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑏 ↔ [ 𝑧 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 )
6	5	rexbii	⊢ ( ∃ 𝑧 ∈ 𝐴 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑏 ↔ ∃ 𝑧 ∈ 𝐴 [ 𝑧 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 )
7		nfs1v	⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑
8		nfv	⊢ Ⅎ 𝑧 [ 𝑏 / 𝑦 ] 𝜑
9		sbequ12r	⊢ ( 𝑧 = 𝑥 → ( [ 𝑧 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑦 ] 𝜑 ) )
10	7 8 9	cbvrexw	⊢ ( ∃ 𝑧 ∈ 𝐴 [ 𝑧 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 [ 𝑏 / 𝑦 ] 𝜑 )
11	2 6 10	3bitri	⊢ ( 𝑏 ∈ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } “ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 [ 𝑏 / 𝑦 ] 𝜑 )

Metamath Proof Explorer

Theorem isarep1

Proof