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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ↔ 𝜓 ) )

Metamath Proof Explorer

Theorem eloprabga

Proof