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