Theorem mobidv 2543

Description: Formula-building rule for the at-most-one quantifier (deduction form). (Contributed by Mario Carneiro, 7-Oct-2016.) Reduce axiom dependencies and shorten proof. (Revised by BJ, 7-Oct-2022.)

Hypothesis

Ref	Expression
mobidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
mobidv	⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem mobidv

Step	Hyp	Ref	Expression
1		mobidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	alrimiv 1927	. 2 ⊢ (𝜑 → ∀𝑥(𝜓 ↔ 𝜒))
3		mobi 2541	. 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
4	2, 3	syl 17	1 ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538  ∃*wmo 2532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2534

This theorem is referenced by:  moanimv  2613  rmobidva  3371  rmoeq1OLD  3392  mosubopt  5473  dffun6f  6532  funmo  6534  funmoOLD  6535  caovmo  7629  1stconst  8082  2ndconst  8083  brdom3  10488  brdom6disj  10492  imasaddfnlem  17498  imasvscafn  17507  hausflim  23875  hausflf  23891  cnextfun  23958  haustsms  24030  limcmo  25790  perfdvf  25811  rmounid  32431  rmoeqbidv  36208  disjeq12dv  36210  phpreu  37605  alrmomodm  38348  funressnfv  47048  funressnmo  47051  mosn  48805  mof02  48831  mofsn2  48837  f1omo  48885  f1omoOLD  48886  isthinc  49412  isthincd2lem1  49418  thincmoALT  49422  thincmod  49423  isthincd  49429  thincpropd  49435  indcthing  49453  discthing  49454  setcthin  49458