Theorem opelopabaf

Description: The law of concretion. Theorem 9.5 of Quine p. 61. This version of opelopab uses bound-variable hypotheses in place of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2013) (Proof shortened by Mario Carneiro, 18-Nov-2016)

	Ref	Expression
Hypotheses	opelopabaf.x	⊢ Ⅎ 𝑥 𝜓
	opelopabaf.y	⊢ Ⅎ 𝑦 𝜓
	opelopabaf.1	⊢ 𝐴 ∈ V
	opelopabaf.2	⊢ 𝐵 ∈ V
	opelopabaf.3	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion	opelopabaf	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		opelopabaf.x	⊢ Ⅎ 𝑥 𝜓
2		opelopabaf.y	⊢ Ⅎ 𝑦 𝜓
3		opelopabaf.1	⊢ 𝐴 ∈ V
4		opelopabaf.2	⊢ 𝐵 ∈ V
5		opelopabaf.3	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜑 ↔ 𝜓 ) )
6		opelopabsb	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 )
7		nfv	⊢ Ⅎ 𝑥 𝐵 ∈ V
8	1 2 7 5	sbc2iegf	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ 𝜓 ) )
9	3 4 8	mp2an	⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ 𝜓 )
10	6 9	bitri	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜓 )