This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ Ⅎ 𝑥 𝜑
Assertion rmoanimALT ( ∃* 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 → ∃* 𝑥 ∈ 𝐴 𝜓 ) )

Proof

Step Hyp Ref Expression
1 rmoanim.1 ⊢ Ⅎ 𝑥 𝜑
2 impexp ⊢ ( ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ↔ ( 𝜑 → ( 𝜓 → 𝑥 = 𝑦 ) ) )
3 2 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → ( 𝜓 → 𝑥 = 𝑦 ) ) )
4 1 r19.21 ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → ( 𝜓 → 𝑥 = 𝑦 ) ) ↔ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) )
5 3 4 bitri ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ↔ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) )
6 5 exbii ⊢ ( ∃ 𝑦 ∀ 𝑥 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ↔ ∃ 𝑦 ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) )
7 nfv ⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝜓 )
8 7 rmo2 ⊢ ( ∃* 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑦 ∀ 𝑥 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) )
9 nfv ⊢ Ⅎ 𝑦 𝜓
10 9 rmo2 ⊢ ( ∃* 𝑥 ∈ 𝐴 𝜓 ↔ ∃ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) )
11 10 imbi2i ⊢ ( ( 𝜑 → ∃* 𝑥 ∈ 𝐴 𝜓 ) ↔ ( 𝜑 → ∃ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) )
12 19.37v ⊢ ( ∃ 𝑦 ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) ↔ ( 𝜑 → ∃ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) )
13 11 12 bitr4i ⊢ ( ( 𝜑 → ∃* 𝑥 ∈ 𝐴 𝜓 ) ↔ ∃ 𝑦 ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) )
14 6 8 13 3bitr4i ⊢ ( ∃* 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 → ∃* 𝑥 ∈ 𝐴 𝜓 ) )