Metamath Proof Explorer

Theorem brxrn2

Description: A characterization of the range Cartesian product. (Contributed by Peter Mazsa, 14-Oct-2020)

Ref Expression
Assertion brxrn2 ⊢ A ∈ V → A R ⋉ S B ↔ ∃ x ∃ y B = x y ∧ A R x ∧ A S y

Proof

Step Hyp Ref Expression
1 xrnss3v ⊢ R ⋉ S ⊆ V × V × V
2 1 brel ⊢ A R ⋉ S B → A ∈ V ∧ B ∈ V × V
3 2 simprd ⊢ A R ⋉ S B → B ∈ V × V
4 elvv ⊢ B ∈ V × V ↔ ∃ x ∃ y B = x y
5 3 4 sylib ⊢ A R ⋉ S B → ∃ x ∃ y B = x y
6 5 pm4.71ri ⊢ A R ⋉ S B ↔ ∃ x ∃ y B = x y ∧ A R ⋉ S B
7 19.41vv ⊢ ∃ x ∃ y B = x y ∧ A R ⋉ S B ↔ ∃ x ∃ y B = x y ∧ A R ⋉ S B
8 breq2 ⊢ B = x y → A R ⋉ S B ↔ A R ⋉ S x y
9 8 pm5.32i ⊢ B = x y ∧ A R ⋉ S B ↔ B = x y ∧ A R ⋉ S x y
10 9 2exbii ⊢ ∃ x ∃ y B = x y ∧ A R ⋉ S B ↔ ∃ x ∃ y B = x y ∧ A R ⋉ S x y
11 6 7 10 3bitr2i ⊢ A R ⋉ S B ↔ ∃ x ∃ y B = x y ∧ A R ⋉ S x y
12 brxrn ⊢ A ∈ V ∧ x ∈ V ∧ y ∈ V → A R ⋉ S x y ↔ A R x ∧ A S y
13 12 el3v23 ⊢ A ∈ V → A R ⋉ S x y ↔ A R x ∧ A S y
14 13 anbi2d ⊢ A ∈ V → B = x y ∧ A R ⋉ S x y ↔ B = x y ∧ A R x ∧ A S y
15 3anass ⊢ B = x y ∧ A R x ∧ A S y ↔ B = x y ∧ A R x ∧ A S y
16 14 15 bitr4di ⊢ A ∈ V → B = x y ∧ A R ⋉ S x y ↔ B = x y ∧ A R x ∧ A S y
17 16 2exbidv ⊢ A ∈ V → ∃ x ∃ y B = x y ∧ A R ⋉ S x y ↔ ∃ x ∃ y B = x y ∧ A R x ∧ A S y
18 11 17 bitrid ⊢ A ∈ V → A R ⋉ S B ↔ ∃ x ∃ y B = x y ∧ A R x ∧ A S y