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

Proof

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