Metamath Proof Explorer

Theorem rexxfr3dALT

Description: Longer proof of rexxfr3d using ax-11 instead of ax-12 , without the disjoint variable condition A x y . (Contributed by SN, 19-Jun-2025) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses rexxfr3dALT.s ⊢ x = X → ψ ↔ χ
rexxfr3dALT.x ⊢ φ → x ∈ A ↔ ∃ y ∈ B x = X
rexxfr3dALT.a ⊢ φ → X ∈ V
Assertion rexxfr3dALT ⊢ φ → ∃ x ∈ A ψ ↔ ∃ y ∈ B χ

Proof

Step Hyp Ref Expression
1 rexxfr3dALT.s ⊢ x = X → ψ ↔ χ
2 rexxfr3dALT.x ⊢ φ → x ∈ A ↔ ∃ y ∈ B x = X
3 rexxfr3dALT.a ⊢ φ → X ∈ V
4 2 anbi1d ⊢ φ → x ∈ A ∧ ψ ↔ ∃ y ∈ B x = X ∧ ψ
5 1 pm5.32i ⊢ x = X ∧ ψ ↔ x = X ∧ χ
6 5 rexbii ⊢ ∃ y ∈ B x = X ∧ ψ ↔ ∃ y ∈ B x = X ∧ χ
7 r19.41v ⊢ ∃ y ∈ B x = X ∧ ψ ↔ ∃ y ∈ B x = X ∧ ψ
8 6 7 bitr3i ⊢ ∃ y ∈ B x = X ∧ χ ↔ ∃ y ∈ B x = X ∧ ψ
9 4 8 bitr4di ⊢ φ → x ∈ A ∧ ψ ↔ ∃ y ∈ B x = X ∧ χ
10 9 exbidv ⊢ φ → ∃ x x ∈ A ∧ ψ ↔ ∃ x ∃ y ∈ B x = X ∧ χ
11 df-rex ⊢ ∃ x ∈ A ψ ↔ ∃ x x ∈ A ∧ ψ
12 19.41v ⊢ ∃ x x = X ∧ χ ↔ ∃ x x = X ∧ χ
13 12 rexbii ⊢ ∃ y ∈ B ∃ x x = X ∧ χ ↔ ∃ y ∈ B ∃ x x = X ∧ χ
14 rexcom4 ⊢ ∃ y ∈ B ∃ x x = X ∧ χ ↔ ∃ x ∃ y ∈ B x = X ∧ χ
15 13 14 bitr3i ⊢ ∃ y ∈ B ∃ x x = X ∧ χ ↔ ∃ x ∃ y ∈ B x = X ∧ χ
16 10 11 15 3bitr4g ⊢ φ → ∃ x ∈ A ψ ↔ ∃ y ∈ B ∃ x x = X ∧ χ
17 elisset ⊢ X ∈ V → ∃ x x = X
18 3 17 syl ⊢ φ → ∃ x x = X
19 18 biantrurd ⊢ φ → χ ↔ ∃ x x = X ∧ χ
20 19 rexbidv ⊢ φ → ∃ y ∈ B χ ↔ ∃ y ∈ B ∃ x x = X ∧ χ
21 16 20 bitr4d ⊢ φ → ∃ x ∈ A ψ ↔ ∃ y ∈ B χ