Metamath Proof Explorer

Theorem cbvrexdva2OLD

Description: Obsolete version of cbvrexdva as of 12-Aug-2023. (Contributed by David Moews, 1-May-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses cbvraldva2.1 ⊢ φ ∧ x = y → ψ ↔ χ
cbvraldva2.2 ⊢ φ ∧ x = y → A = B
Assertion cbvrexdva2OLD ⊢ φ → ∃ x ∈ A ψ ↔ ∃ y ∈ B χ

Proof

Step Hyp Ref Expression
1 cbvraldva2.1 ⊢ φ ∧ x = y → ψ ↔ χ
2 cbvraldva2.2 ⊢ φ ∧ x = y → A = B
3 simpr ⊢ φ ∧ x = y → x = y
4 3 2 eleq12d ⊢ φ ∧ x = y → x ∈ A ↔ y ∈ B
5 4 1 anbi12d ⊢ φ ∧ x = y → x ∈ A ∧ ψ ↔ y ∈ B ∧ χ
6 5 notbid ⊢ φ ∧ x = y → ¬ x ∈ A ∧ ψ ↔ ¬ y ∈ B ∧ χ
7 6 expcom ⊢ x = y → φ → ¬ x ∈ A ∧ ψ ↔ ¬ y ∈ B ∧ χ
8 7 pm5.74d ⊢ x = y → φ → ¬ x ∈ A ∧ ψ ↔ φ → ¬ y ∈ B ∧ χ
9 8 cbvalvw ⊢ ∀ x φ → ¬ x ∈ A ∧ ψ ↔ ∀ y φ → ¬ y ∈ B ∧ χ
10 19.21v ⊢ ∀ x φ → ¬ x ∈ A ∧ ψ ↔ φ → ∀ x ¬ x ∈ A ∧ ψ
11 19.21v ⊢ ∀ y φ → ¬ y ∈ B ∧ χ ↔ φ → ∀ y ¬ y ∈ B ∧ χ
12 9 10 11 3bitr3i ⊢ φ → ∀ x ¬ x ∈ A ∧ ψ ↔ φ → ∀ y ¬ y ∈ B ∧ χ
13 12 pm5.74ri ⊢ φ → ∀ x ¬ x ∈ A ∧ ψ ↔ ∀ y ¬ y ∈ B ∧ χ
14 alnex ⊢ ∀ x ¬ x ∈ A ∧ ψ ↔ ¬ ∃ x x ∈ A ∧ ψ
15 alnex ⊢ ∀ y ¬ y ∈ B ∧ χ ↔ ¬ ∃ y y ∈ B ∧ χ
16 13 14 15 3bitr3g ⊢ φ → ¬ ∃ x x ∈ A ∧ ψ ↔ ¬ ∃ y y ∈ B ∧ χ
17 16 con4bid ⊢ φ → ∃ x x ∈ A ∧ ψ ↔ ∃ y y ∈ B ∧ χ
18 df-rex ⊢ ∃ x ∈ A ψ ↔ ∃ x x ∈ A ∧ ψ
19 df-rex ⊢ ∃ y ∈ B χ ↔ ∃ y y ∈ B ∧ χ
20 17 18 19 3bitr4g ⊢ φ → ∃ x ∈ A ψ ↔ ∃ y ∈ B χ