Metamath Proof Explorer

Theorem elxp6

Description: Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 . (Contributed by NM, 9-Oct-2004)

Ref Expression
Assertion elxp6 ⊢ A ∈ B × C ↔ A = 1 st ⁡ A 2 nd ⁡ A ∧ 1 st ⁡ A ∈ B ∧ 2 nd ⁡ A ∈ C

Proof

Step Hyp Ref Expression
1 elxp4 ⊢ A ∈ B × C ↔ A = ⋃ dom ⁡ A ⋃ ran ⁡ A ∧ ⋃ dom ⁡ A ∈ B ∧ ⋃ ran ⁡ A ∈ C
2 1stval ⊢ 1 st ⁡ A = ⋃ dom ⁡ A
3 2ndval ⊢ 2 nd ⁡ A = ⋃ ran ⁡ A
4 2 3 opeq12i ⊢ 1 st ⁡ A 2 nd ⁡ A = ⋃ dom ⁡ A ⋃ ran ⁡ A
5 4 eqeq2i ⊢ A = 1 st ⁡ A 2 nd ⁡ A ↔ A = ⋃ dom ⁡ A ⋃ ran ⁡ A
6 2 eleq1i ⊢ 1 st ⁡ A ∈ B ↔ ⋃ dom ⁡ A ∈ B
7 3 eleq1i ⊢ 2 nd ⁡ A ∈ C ↔ ⋃ ran ⁡ A ∈ C
8 6 7 anbi12i ⊢ 1 st ⁡ A ∈ B ∧ 2 nd ⁡ A ∈ C ↔ ⋃ dom ⁡ A ∈ B ∧ ⋃ ran ⁡ A ∈ C
9 5 8 anbi12i ⊢ A = 1 st ⁡ A 2 nd ⁡ A ∧ 1 st ⁡ A ∈ B ∧ 2 nd ⁡ A ∈ C ↔ A = ⋃ dom ⁡ A ⋃ ran ⁡ A ∧ ⋃ dom ⁡ A ∈ B ∧ ⋃ ran ⁡ A ∈ C
10 1 9 bitr4i ⊢ A ∈ B × C ↔ A = 1 st ⁡ A 2 nd ⁡ A ∧ 1 st ⁡ A ∈ B ∧ 2 nd ⁡ A ∈ C