Metamath Proof Explorer

Theorem rmoanimALT

Description: Alternate proof of rmoanim , shorter but requiring ax-10 and ax-11 . (Contributed by Alexander van der Vekens, 25-Jun-2017) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis rmoanim.1 ⊢ Ⅎ x φ
Assertion rmoanimALT ⊢ ∃* x ∈ A φ ∧ ψ ↔ φ → ∃* x ∈ A ψ

Proof

Step Hyp Ref Expression
1 rmoanim.1 ⊢ Ⅎ x φ
2 impexp ⊢ φ ∧ ψ → x = y ↔ φ → ψ → x = y
3 2 ralbii ⊢ ∀ x ∈ A φ ∧ ψ → x = y ↔ ∀ x ∈ A φ → ψ → x = y
4 1 r19.21 ⊢ ∀ x ∈ A φ → ψ → x = y ↔ φ → ∀ x ∈ A ψ → x = y
5 3 4 bitri ⊢ ∀ x ∈ A φ ∧ ψ → x = y ↔ φ → ∀ x ∈ A ψ → x = y
6 5 exbii ⊢ ∃ y ∀ x ∈ A φ ∧ ψ → x = y ↔ ∃ y φ → ∀ x ∈ A ψ → x = y
7 nfv ⊢ Ⅎ y φ ∧ ψ
8 7 rmo2 ⊢ ∃* x ∈ A φ ∧ ψ ↔ ∃ y ∀ x ∈ A φ ∧ ψ → x = y
9 nfv ⊢ Ⅎ y ψ
10 9 rmo2 ⊢ ∃* x ∈ A ψ ↔ ∃ y ∀ x ∈ A ψ → x = y
11 10 imbi2i ⊢ φ → ∃* x ∈ A ψ ↔ φ → ∃ y ∀ x ∈ A ψ → x = y
12 19.37v ⊢ ∃ y φ → ∀ x ∈ A ψ → x = y ↔ φ → ∃ y ∀ x ∈ A ψ → x = y
13 11 12 bitr4i ⊢ φ → ∃* x ∈ A ψ ↔ ∃ y φ → ∀ x ∈ A ψ → x = y
14 6 8 13 3bitr4i ⊢ ∃* x ∈ A φ ∧ ψ ↔ φ → ∃* x ∈ A ψ