Theorem isarep1OLD

Description: Obsolete version of isarep1 as of 19-Dec-2024. (Contributed by NM, 26-Oct-2006) (Proof shortened by Mario Carneiro, 4-Dec-2016) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	isarep1OLD	⊢ ( 𝑏 ∈ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } “ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 [ 𝑏 / 𝑦 ] 𝜑 )

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