This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝜑 ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) }