Theorem mobidv 2574

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-mo 2564

This theorem is used by:  moanimv  2644  rmobidva  3378  mosubopt  5481  mosubott  5483  dffun6f  6553  funmo  6554  caovmo  7658  1stconst  8113  2ndconst  8114  brdom3  10610  brdom6disj  10614  imasaddfnlem  17705  imasvscafn  17714  hausflim  24305  hausflf  24321  cnextfun  24388  haustsms  24460  limcmo  26207  perfdvf  26228  rmounid  33138  rmoeqbidv  37094  disjeq12dv  37096  phpreu  38620  alrmomodm  39384  funressnfv  48206  funressnmo  48209  mosn  50017  mof02  50043  mofsn2  50049  f1omo  50100  f1omoOLD  50101  isthinc  50647  isthincd2lem1  50653  thincmoALT  50657  thincmod  50658  isthincd  50664  thincpropd  50670  indcthing  50688  discthing  50689  setcthin  50693