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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537  ∃*wmo 2538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-mo 2540

This theorem is referenced by:  moanimv  2621  rmoeq1  3336  mosubopt  5418  dffun6f  6432  funmo  6434  caovmo  7487  1stconst  7911  2ndconst  7912  brdom3  10215  brdom6disj  10219  imasaddfnlem  17156  imasvscafn  17165  hausflim  23040  hausflf  23056  cnextfun  23123  haustsms  23195  limcmo  24951  perfdvf  24972  rmounid  30744  phpreu  35688  alrmomodm  36418  funressnfv  44424  funressnmo  44427  mosn  46046  mof02  46054  mofsn2  46060  f1omo  46076  isthinc  46190  isthincd2lem1  46196  thincmoALT  46199  thincmod  46200  isthincd  46206  setcthin  46224