Theorem mobidv 2544

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1540  ∃*wmo 2533

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-mo 2535

This theorem is referenced by:  moanimv  2616  rmobidva  3392  rmoeq1OLD  3417  mosubopt  5511  dffun6f  6562  funmo  6564  funmoOLD  6565  caovmo  7644  1stconst  8086  2ndconst  8087  brdom3  10523  brdom6disj  10527  imasaddfnlem  17474  imasvscafn  17483  hausflim  23485  hausflf  23501  cnextfun  23568  haustsms  23640  limcmo  25399  perfdvf  25420  rmounid  31735  phpreu  36472  alrmomodm  37228  funressnfv  45753  funressnmo  45756  mosn  47497  mof02  47505  mofsn2  47511  f1omo  47527  isthinc  47641  isthincd2lem1  47647  thincmoALT  47650  thincmod  47651  isthincd  47657  setcthin  47675