# 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}\in \left({B}×{C}\right)↔\left({A}=⟨{1}^{st}\left({A}\right),{2}^{nd}\left({A}\right)⟩\wedge \left({1}^{st}\left({A}\right)\in {B}\wedge {2}^{nd}\left({A}\right)\in {C}\right)\right)$

### Proof

Step Hyp Ref Expression
1 elxp4 ${⊢}{A}\in \left({B}×{C}\right)↔\left({A}=⟨\bigcup \mathrm{dom}\left\{{A}\right\},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\wedge \left(\bigcup \mathrm{dom}\left\{{A}\right\}\in {B}\wedge \bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)\right)$
2 1stval ${⊢}{1}^{st}\left({A}\right)=\bigcup \mathrm{dom}\left\{{A}\right\}$
3 2ndval ${⊢}{2}^{nd}\left({A}\right)=\bigcup \mathrm{ran}\left\{{A}\right\}$
4 2 3 opeq12i ${⊢}⟨{1}^{st}\left({A}\right),{2}^{nd}\left({A}\right)⟩=⟨\bigcup \mathrm{dom}\left\{{A}\right\},\bigcup \mathrm{ran}\left\{{A}\right\}⟩$
5 4 eqeq2i ${⊢}{A}=⟨{1}^{st}\left({A}\right),{2}^{nd}\left({A}\right)⟩↔{A}=⟨\bigcup \mathrm{dom}\left\{{A}\right\},\bigcup \mathrm{ran}\left\{{A}\right\}⟩$
6 2 eleq1i ${⊢}{1}^{st}\left({A}\right)\in {B}↔\bigcup \mathrm{dom}\left\{{A}\right\}\in {B}$
7 3 eleq1i ${⊢}{2}^{nd}\left({A}\right)\in {C}↔\bigcup \mathrm{ran}\left\{{A}\right\}\in {C}$
8 6 7 anbi12i ${⊢}\left({1}^{st}\left({A}\right)\in {B}\wedge {2}^{nd}\left({A}\right)\in {C}\right)↔\left(\bigcup \mathrm{dom}\left\{{A}\right\}\in {B}\wedge \bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)$
9 5 8 anbi12i ${⊢}\left({A}=⟨{1}^{st}\left({A}\right),{2}^{nd}\left({A}\right)⟩\wedge \left({1}^{st}\left({A}\right)\in {B}\wedge {2}^{nd}\left({A}\right)\in {C}\right)\right)↔\left({A}=⟨\bigcup \mathrm{dom}\left\{{A}\right\},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\wedge \left(\bigcup \mathrm{dom}\left\{{A}\right\}\in {B}\wedge \bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)\right)$
10 1 9 bitr4i ${⊢}{A}\in \left({B}×{C}\right)↔\left({A}=⟨{1}^{st}\left({A}\right),{2}^{nd}\left({A}\right)⟩\wedge \left({1}^{st}\left({A}\right)\in {B}\wedge {2}^{nd}\left({A}\right)\in {C}\right)\right)$