Theorem mobidv 2580

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

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

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 1943  ax-6 2000  ax-7 2041

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

This theorem is used by:  moanimv  2650  rmobidva  3385  mosubopt  5498  dffun6f  6558  funmo  6559  caovmo  7660  1stconst  8104  2ndconst  8105  brdom3  10530  brdom6disj  10534  imasaddfnlem  17607  imasvscafn  17616  hausflim  24175  hausflf  24191  cnextfun  24258  haustsms  24330  limcmo  26078  perfdvf  26099  rmounid  32878  rmoeqbidv  36766  disjeq12dv  36768  phpreu  38296  alrmomodm  39049  funressnfv  47821  funressnmo  47824  mosn  49632  mof02  49658  mofsn2  49664  f1omo  49712  f1omoOLD  49713  isthinc  50238  isthincd2lem1  50244  thincmoALT  50248  thincmod  50249  isthincd  50255  thincpropd  50261  indcthing  50279  discthing  50280  setcthin  50284