Metamath Proof Explorer

Theorem elxp7

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

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

Proof

Step Hyp Ref Expression
1 elxp6 ⊢ A ∈ B × C ↔ A = 1 st ⁡ A 2 nd ⁡ A ∧ 1 st ⁡ A ∈ B ∧ 2 nd ⁡ A ∈ C
2 fvex ⊢ 1 st ⁡ A ∈ V
3 fvex ⊢ 2 nd ⁡ A ∈ V
4 2 3 pm3.2i ⊢ 1 st ⁡ A ∈ V ∧ 2 nd ⁡ A ∈ V
5 elxp6 ⊢ A ∈ V × V ↔ A = 1 st ⁡ A 2 nd ⁡ A ∧ 1 st ⁡ A ∈ V ∧ 2 nd ⁡ A ∈ V
6 4 5 mpbiran2 ⊢ A ∈ V × V ↔ A = 1 st ⁡ A 2 nd ⁡ A
7 6 anbi1i ⊢ A ∈ V × V ∧ 1 st ⁡ A ∈ B ∧ 2 nd ⁡ A ∈ C ↔ A = 1 st ⁡ A 2 nd ⁡ A ∧ 1 st ⁡ A ∈ B ∧ 2 nd ⁡ A ∈ C
8 1 7 bitr4i ⊢ A ∈ B × C ↔ A ∈ V × V ∧ 1 st ⁡ A ∈ B ∧ 2 nd ⁡ A ∈ C