mormo - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mormo		Structured version Visualization version GIF version

Theorem mormo 3378

Description: Unrestricted "at most one" implies restricted "at most one". (Contributed by NM, 16-Jun-2017.)

**Assertion**
Ref	Expression
mormo	⊢ (∃𝑥𝜑 → ∃𝑥 ∈ 𝐴 𝜑)

**Proof of Theorem mormo**
Step	Hyp	Ref	Expression
1		moan 2542	. 2 ⊢ (∃𝑥𝜑 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
2		df-rmo 3373	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3	1, 2	sylibr 233	1 ⊢ (∃𝑥𝜑 → ∃𝑥 ∈ 𝐴 𝜑)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2099 ∃*wmo 2528 ∃*wrmo 3372

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804

This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1775 df-mo 2530 df-rmo 3373

This theorem is referenced by: reueq 3732 reusv1 5397 brdom4 10553 phpreu 37077

	
		OSZAR »