Metamath Proof Explorer

Theorem rexopabb

Description: Restricted existential quantification over an ordered-pair class abstraction. (Contributed by AV, 8-Nov-2023)

Ref Expression
Hypotheses rexopabb.o ⊢ O = x y | φ
rexopabb.p ⊢ o = x y → ψ ↔ χ
Assertion rexopabb ⊢ ∃ o ∈ O ψ ↔ ∃ x ∃ y φ ∧ χ

Proof

Step Hyp Ref Expression
1 rexopabb.o ⊢ O = x y | φ
2 rexopabb.p ⊢ o = x y → ψ ↔ χ
3 1 rexeqi ⊢ ∃ o ∈ O ψ ↔ ∃ o ∈ x y | φ ψ
4 elopab ⊢ o ∈ x y | φ ↔ ∃ x ∃ y o = x y ∧ φ
5 simprr ⊢ ψ ∧ o = x y ∧ φ → φ
6 2 biimpd ⊢ o = x y → ψ → χ
7 6 adantr ⊢ o = x y ∧ φ → ψ → χ
8 7 impcom ⊢ ψ ∧ o = x y ∧ φ → χ
9 5 8 jca ⊢ ψ ∧ o = x y ∧ φ → φ ∧ χ
10 9 ex ⊢ ψ → o = x y ∧ φ → φ ∧ χ
11 10 2eximdv ⊢ ψ → ∃ x ∃ y o = x y ∧ φ → ∃ x ∃ y φ ∧ χ
12 11 impcom ⊢ ∃ x ∃ y o = x y ∧ φ ∧ ψ → ∃ x ∃ y φ ∧ χ
13 4 12 sylanb ⊢ o ∈ x y | φ ∧ ψ → ∃ x ∃ y φ ∧ χ
14 13 rexlimiva ⊢ ∃ o ∈ x y | φ ψ → ∃ x ∃ y φ ∧ χ
15 nfopab1 ⊢ Ⅎ _ x x y | φ
16 nfv ⊢ Ⅎ x ψ
17 15 16 nfrex ⊢ Ⅎ x ∃ o ∈ x y | φ ψ
18 nfopab2 ⊢ Ⅎ _ y x y | φ
19 nfv ⊢ Ⅎ y ψ
20 18 19 nfrex ⊢ Ⅎ y ∃ o ∈ x y | φ ψ
21 opabidw ⊢ x y ∈ x y | φ ↔ φ
22 opex ⊢ x y ∈ V
23 22 2 sbcie ⊢ [˙ x y / o]˙ ψ ↔ χ
24 rspesbca ⊢ x y ∈ x y | φ ∧ [˙ x y / o]˙ ψ → ∃ o ∈ x y | φ ψ
25 21 23 24 syl2anbr ⊢ φ ∧ χ → ∃ o ∈ x y | φ ψ
26 20 25 exlimi ⊢ ∃ y φ ∧ χ → ∃ o ∈ x y | φ ψ
27 17 26 exlimi ⊢ ∃ x ∃ y φ ∧ χ → ∃ o ∈ x y | φ ψ
28 14 27 impbii ⊢ ∃ o ∈ x y | φ ψ ↔ ∃ x ∃ y φ ∧ χ
29 3 28 bitri ⊢ ∃ o ∈ O ψ ↔ ∃ x ∃ y φ ∧ χ