Theorem dfoprab4f

Description: Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 20-Dec-2008) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypotheses	dfoprab4f.x	⊢ Ⅎ 𝑥 𝜑
	dfoprab4f.y	⊢ Ⅎ 𝑦 𝜑
	dfoprab4f.1	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ 𝜓 ) )
Assertion	dfoprab4f	⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝜑 ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) }

Proof

Step	Hyp	Ref	Expression
1		dfoprab4f.x	⊢ Ⅎ 𝑥 𝜑
2		dfoprab4f.y	⊢ Ⅎ 𝑦 𝜑
3		dfoprab4f.1	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ 𝜓 ) )
4		nfv	⊢ Ⅎ 𝑥 𝑤 = ⟨ 𝑡 , 𝑢 ⟩
5		nfs1v	⊢ Ⅎ 𝑥 [ 𝑡 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓
6	1 5	nfbi	⊢ Ⅎ 𝑥 ( 𝜑 ↔ [ 𝑡 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓 )
7	4 6	nfim	⊢ Ⅎ 𝑥 ( 𝑤 = ⟨ 𝑡 , 𝑢 ⟩ → ( 𝜑 ↔ [ 𝑡 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓 ) )
8		opeq1	⊢ ( 𝑥 = 𝑡 → ⟨ 𝑥 , 𝑢 ⟩ = ⟨ 𝑡 , 𝑢 ⟩ )
9	8	eqeq2d	⊢ ( 𝑥 = 𝑡 → ( 𝑤 = ⟨ 𝑥 , 𝑢 ⟩ ↔ 𝑤 = ⟨ 𝑡 , 𝑢 ⟩ ) )
10		sbequ12	⊢ ( 𝑥 = 𝑡 → ( [ 𝑢 / 𝑦 ] 𝜓 ↔ [ 𝑡 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓 ) )
11	10	bibi2d	⊢ ( 𝑥 = 𝑡 → ( ( 𝜑 ↔ [ 𝑢 / 𝑦 ] 𝜓 ) ↔ ( 𝜑 ↔ [ 𝑡 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓 ) ) )
12	9 11	imbi12d	⊢ ( 𝑥 = 𝑡 → ( ( 𝑤 = ⟨ 𝑥 , 𝑢 ⟩ → ( 𝜑 ↔ [ 𝑢 / 𝑦 ] 𝜓 ) ) ↔ ( 𝑤 = ⟨ 𝑡 , 𝑢 ⟩ → ( 𝜑 ↔ [ 𝑡 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓 ) ) ) )
13		nfv	⊢ Ⅎ 𝑦 𝑤 = ⟨ 𝑥 , 𝑢 ⟩
14		nfs1v	⊢ Ⅎ 𝑦 [ 𝑢 / 𝑦 ] 𝜓
15	2 14	nfbi	⊢ Ⅎ 𝑦 ( 𝜑 ↔ [ 𝑢 / 𝑦 ] 𝜓 )
16	13 15	nfim	⊢ Ⅎ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑢 ⟩ → ( 𝜑 ↔ [ 𝑢 / 𝑦 ] 𝜓 ) )
17		opeq2	⊢ ( 𝑦 = 𝑢 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑢 ⟩ )
18	17	eqeq2d	⊢ ( 𝑦 = 𝑢 → ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑤 = ⟨ 𝑥 , 𝑢 ⟩ ) )
19		sbequ12	⊢ ( 𝑦 = 𝑢 → ( 𝜓 ↔ [ 𝑢 / 𝑦 ] 𝜓 ) )
20	19	bibi2d	⊢ ( 𝑦 = 𝑢 → ( ( 𝜑 ↔ 𝜓 ) ↔ ( 𝜑 ↔ [ 𝑢 / 𝑦 ] 𝜓 ) ) )
21	18 20	imbi12d	⊢ ( 𝑦 = 𝑢 → ( ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ 𝜓 ) ) ↔ ( 𝑤 = ⟨ 𝑥 , 𝑢 ⟩ → ( 𝜑 ↔ [ 𝑢 / 𝑦 ] 𝜓 ) ) ) )
22	16 21 3	chvarfv	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑢 ⟩ → ( 𝜑 ↔ [ 𝑢 / 𝑦 ] 𝜓 ) )
23	7 12 22	chvarfv	⊢ ( 𝑤 = ⟨ 𝑡 , 𝑢 ⟩ → ( 𝜑 ↔ [ 𝑡 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓 ) )
24	23	dfoprab4	⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝜑 ) } = { ⟨ ⟨ 𝑡 , 𝑢 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ [ 𝑡 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓 ) }
25		nfv	⊢ Ⅎ 𝑡 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 )
26		nfv	⊢ Ⅎ 𝑢 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 )
27		nfv	⊢ Ⅎ 𝑥 ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 )
28	27 5	nfan	⊢ Ⅎ 𝑥 ( ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ [ 𝑡 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓 )
29		nfv	⊢ Ⅎ 𝑦 ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 )
30	14	nfsbv	⊢ Ⅎ 𝑦 [ 𝑡 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓
31	29 30	nfan	⊢ Ⅎ 𝑦 ( ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ [ 𝑡 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓 )
32		eleq1w	⊢ ( 𝑥 = 𝑡 → ( 𝑥 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴 ) )
33		eleq1w	⊢ ( 𝑦 = 𝑢 → ( 𝑦 ∈ 𝐵 ↔ 𝑢 ∈ 𝐵 ) )
34	32 33	bi2anan9	⊢ ( ( 𝑥 = 𝑡 ∧ 𝑦 = 𝑢 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ) )
35	19 10	sylan9bbr	⊢ ( ( 𝑥 = 𝑡 ∧ 𝑦 = 𝑢 ) → ( 𝜓 ↔ [ 𝑡 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓 ) )
36	34 35	anbi12d	⊢ ( ( 𝑥 = 𝑡 ∧ 𝑦 = 𝑢 ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) ↔ ( ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ [ 𝑡 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓 ) ) )
37	25 26 28 31 36	cbvoprab12	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) } = { ⟨ ⟨ 𝑡 , 𝑢 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ [ 𝑡 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓 ) }
38	24 37	eqtr4i	⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝜑 ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) }