Theorem mobidv 2542

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

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

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 2533

This theorem is referenced by:  moanimv  2612  rmobidva  3360  rmoeq1OLD  3380  mosubopt  5457  dffun6f  6501  funmo  6502  caovmo  7590  1stconst  8040  2ndconst  8041  brdom3  10441  brdom6disj  10445  imasaddfnlem  17450  imasvscafn  17459  hausflim  23884  hausflf  23900  cnextfun  23967  haustsms  24039  limcmo  25799  perfdvf  25820  rmounid  32457  rmoeqbidv  36186  disjeq12dv  36188  phpreu  37583  alrmomodm  38326  funressnfv  47028  funressnmo  47031  mosn  48798  mof02  48824  mofsn2  48830  f1omo  48878  f1omoOLD  48879  isthinc  49405  isthincd2lem1  49411  thincmoALT  49415  thincmod  49416  isthincd  49422  thincpropd  49428  indcthing  49446  discthing  49447  setcthin  49451