Theorem opelopabsbALT

Description: The law of concretion in terms of substitutions. Less general than opelopabsb , but having a much shorter proof. (Contributed by NM, 30-Sep-2002) (Proof shortened by Andrew Salmon, 25-Jul-2011) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	opelopabsbALT	⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		excom	⊢ ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑦 ∃ 𝑥 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
2		vex	⊢ 𝑧 ∈ V
3		vex	⊢ 𝑤 ∈ V
4	2 3	opth	⊢ ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) )
5		equcom	⊢ ( 𝑧 = 𝑥 ↔ 𝑥 = 𝑧 )
6		equcom	⊢ ( 𝑤 = 𝑦 ↔ 𝑦 = 𝑤 )
7	5 6	anbi12ci	⊢ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ↔ ( 𝑦 = 𝑤 ∧ 𝑥 = 𝑧 ) )
8	4 7	bitri	⊢ ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝑦 = 𝑤 ∧ 𝑥 = 𝑧 ) )
9	8	anbi1i	⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( ( 𝑦 = 𝑤 ∧ 𝑥 = 𝑧 ) ∧ 𝜑 ) )
10	9	2exbii	⊢ ( ∃ 𝑦 ∃ 𝑥 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑦 ∃ 𝑥 ( ( 𝑦 = 𝑤 ∧ 𝑥 = 𝑧 ) ∧ 𝜑 ) )
11	1 10	bitri	⊢ ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑦 ∃ 𝑥 ( ( 𝑦 = 𝑤 ∧ 𝑥 = 𝑧 ) ∧ 𝜑 ) )
12		elopab	⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
13		2sb5	⊢ ( [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 ↔ ∃ 𝑦 ∃ 𝑥 ( ( 𝑦 = 𝑤 ∧ 𝑥 = 𝑧 ) ∧ 𝜑 ) )
14	11 12 13	3bitr4i	⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 )