Metamath Proof Explorer

Theorem eloprabga

Description: The law of concretion for operation class abstraction. Compare elopab . (Contributed by NM, 14-Sep-1999) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012) (Revised by Mario Carneiro, 19-Dec-2013) Avoid ax-10 , ax-11 . (Revised by Wolf Lammen, 15-Oct-2024)

Ref Expression
Hypothesis eloprabga.1 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion eloprabga ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ↔ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 eloprabga.1 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) → ( 𝜑 ↔ 𝜓 ) )
2 elex ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
3 elex ⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ V )
4 elex ⊢ ( 𝐶 ∈ 𝑋 → 𝐶 ∈ V )
5 opex ⊢ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ V
6 simpr ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) ∧ 𝑤 = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ) → 𝑤 = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ )
7 6 eqeq1d ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) ∧ 𝑤 = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ) → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) )
8 eqcom ⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ )
9 vex ⊢ 𝑥 ∈ V
10 vex ⊢ 𝑦 ∈ V
11 vex ⊢ 𝑧 ∈ V
12 9 10 11 otth2 ⊢ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ↔ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) )
13 8 12 bitri ⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) )
14 7 13 bitrdi ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) ∧ 𝑤 = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ) → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ) )
15 14 anbi1d ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) ∧ 𝑤 = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ) → ( ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ 𝜑 ) ) )
16 1 pm5.32i ⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ 𝜑 ) ↔ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ 𝜓 ) )
17 15 16 bitrdi ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) ∧ 𝑤 = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ) → ( ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ 𝜓 ) ) )
18 17 3exbidv ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) ∧ 𝑤 = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ) → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ 𝜓 ) ) )
19 df-oprab ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) }
20 19 eleq2i ⊢ ( 𝑤 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ↔ 𝑤 ∈ { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) } )
21 abid ⊢ ( 𝑤 ∈ { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) } ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
22 20 21 bitr2i ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ 𝑤 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } )
23 eleq1 ⊢ ( 𝑤 = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ → ( 𝑤 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ) )
24 22 23 bitrid ⊢ ( 𝑤 = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ) )
25 24 adantl ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) ∧ 𝑤 = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ) → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ) )
26 19.41vvv ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ 𝜓 ) ↔ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ 𝜓 ) )
27 elisset ⊢ ( 𝐴 ∈ V → ∃ 𝑥 𝑥 = 𝐴 )
28 elisset ⊢ ( 𝐵 ∈ V → ∃ 𝑦 𝑦 = 𝐵 )
29 elisset ⊢ ( 𝐶 ∈ V → ∃ 𝑧 𝑧 = 𝐶 )
30 27 28 29 3anim123i ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( ∃ 𝑥 𝑥 = 𝐴 ∧ ∃ 𝑦 𝑦 = 𝐵 ∧ ∃ 𝑧 𝑧 = 𝐶 ) )
31 3exdistr ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ ∃ 𝑧 𝑧 = 𝐶 ) ) )
32 19.41v ⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ ∃ 𝑧 𝑧 = 𝐶 ) ) ↔ ( ∃ 𝑥 𝑥 = 𝐴 ∧ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ ∃ 𝑧 𝑧 = 𝐶 ) ) )
33 19.41v ⊢ ( ∃ 𝑦 ( 𝑦 = 𝐵 ∧ ∃ 𝑧 𝑧 = 𝐶 ) ↔ ( ∃ 𝑦 𝑦 = 𝐵 ∧ ∃ 𝑧 𝑧 = 𝐶 ) )
34 33 anbi2i ⊢ ( ( ∃ 𝑥 𝑥 = 𝐴 ∧ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ ∃ 𝑧 𝑧 = 𝐶 ) ) ↔ ( ∃ 𝑥 𝑥 = 𝐴 ∧ ( ∃ 𝑦 𝑦 = 𝐵 ∧ ∃ 𝑧 𝑧 = 𝐶 ) ) )
35 31 32 34 3bitri ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ↔ ( ∃ 𝑥 𝑥 = 𝐴 ∧ ( ∃ 𝑦 𝑦 = 𝐵 ∧ ∃ 𝑧 𝑧 = 𝐶 ) ) )
36 3anass ⊢ ( ( ∃ 𝑥 𝑥 = 𝐴 ∧ ∃ 𝑦 𝑦 = 𝐵 ∧ ∃ 𝑧 𝑧 = 𝐶 ) ↔ ( ∃ 𝑥 𝑥 = 𝐴 ∧ ( ∃ 𝑦 𝑦 = 𝐵 ∧ ∃ 𝑧 𝑧 = 𝐶 ) ) )
37 35 36 bitr4i ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ↔ ( ∃ 𝑥 𝑥 = 𝐴 ∧ ∃ 𝑦 𝑦 = 𝐵 ∧ ∃ 𝑧 𝑧 = 𝐶 ) )
38 30 37 sylibr ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) )
39 38 biantrurd ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( 𝜓 ↔ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ 𝜓 ) ) )
40 26 39 bitr4id ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ 𝜓 ) ↔ 𝜓 ) )
41 40 adantr ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) ∧ 𝑤 = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ) → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ 𝜓 ) ↔ 𝜓 ) )
42 18 25 41 3bitr3d ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) ∧ 𝑤 = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ↔ 𝜓 ) )
43 42 expcom ⊢ ( 𝑤 = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ → ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ↔ 𝜓 ) ) )
44 5 43 vtocle ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ↔ 𝜓 ) )
45 2 3 4 44 syl3an ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ↔ 𝜓 ) )