Theorem opelopabgf

Description: The law of concretion. Theorem 9.5 of Quine p. 61. This version of opelopabg uses bound-variable hypotheses in place of distinct variable conditions. (Contributed by Alexander van der Vekens, 8-Jul-2018)

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

Proof

Step	Hyp	Ref	Expression
1		opelopabgf.x	⊢ Ⅎ 𝑥 𝜓
2		opelopabgf.y	⊢ Ⅎ 𝑦 𝜒
3		opelopabgf.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
4		opelopabgf.2	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
5		opelopabsb	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 )
6		nfcv	⊢ Ⅎ 𝑥 𝐵
7	6 1	nfsbcw	⊢ Ⅎ 𝑥 [ 𝐵 / 𝑦 ] 𝜓
8	3	sbcbidv	⊢ ( 𝑥 = 𝐴 → ( [ 𝐵 / 𝑦 ] 𝜑 ↔ [ 𝐵 / 𝑦 ] 𝜓 ) )
9	7 8	sbciegf	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ 𝐵 / 𝑦 ] 𝜓 ) )
10	2 4	sbciegf	⊢ ( 𝐵 ∈ 𝑊 → ( [ 𝐵 / 𝑦 ] 𝜓 ↔ 𝜒 ) )
11	9 10	sylan9bb	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ 𝜒 ) )
12	5 11	bitrid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜒 ) )