Theorem mobidv 2549

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539  ∃*wmo 2537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-mo 2539

This theorem is referenced by:  moanimv  2619  rmobidva  3363  rmoeq1OLD  3383  mosubopt  5458  dffun6f  6507  funmo  6508  caovmo  7595  1stconst  8042  2ndconst  8043  brdom3  10438  brdom6disj  10442  imasaddfnlem  17449  imasvscafn  17458  hausflim  23925  hausflf  23941  cnextfun  24008  haustsms  24080  limcmo  25839  perfdvf  25860  rmounid  32569  rmoeqbidv  36407  disjeq12dv  36409  phpreu  37801  alrmomodm  38548  funressnfv  47285  funressnmo  47288  mosn  49054  mof02  49080  mofsn2  49086  f1omo  49134  f1omoOLD  49135  isthinc  49660  isthincd2lem1  49666  thincmoALT  49670  thincmod  49671  isthincd  49677  thincpropd  49683  indcthing  49701  discthing  49702  setcthin  49706