Theorem mobidv 2577

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 1962	. 2 ⊢ (𝜑 → ∀𝑥(𝜓 ↔ 𝜒))
3		mobi 2575	. 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
4	2, 3	syl 18	1 ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568  ∃*wmo 2565

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2567

This theorem is used by:  moanimv  2647  rmobidva  3382  mosubopt  5487  mosubott  5489  dffun6f  6576  funmo  6577  caovmo  7685  1stconst  8141  2ndconst  8142  brdom3  10637  brdom6disj  10641  imasaddfnlem  17732  imasvscafn  17741  hausflim  24333  hausflf  24349  cnextfun  24416  haustsms  24488  limcmo  26235  perfdvf  26256  rmounid  33166  rmoeqbidv  37193  disjeq12dv  37195  phpreu  38732  alrmomodm  39494  funressnfv  48328  funressnmo  48331  mosn  50139  mof02  50165  mofsn2  50171  f1omo  50222  f1omoOLD  50223  isthinc  50769  isthincd2lem1  50775  thincmoALT  50779  thincmod  50780  isthincd  50786  thincpropd  50792  indcthing  50810  discthing  50811  setcthin  50815