Theorem mobidv 2552

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1535  ∃*wmo 2541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-mo 2543

This theorem is referenced by:  moanimv  2622  rmobidva  3403  rmoeq1OLD  3427  mosubopt  5529  dffun6f  6591  funmo  6593  funmoOLD  6594  caovmo  7687  1stconst  8141  2ndconst  8142  brdom3  10597  brdom6disj  10601  imasaddfnlem  17588  imasvscafn  17597  hausflim  24010  hausflf  24026  cnextfun  24093  haustsms  24165  limcmo  25937  perfdvf  25958  rmounid  32523  rmoeqbidv  36177  disjeq12dv  36181  phpreu  37564  alrmomodm  38315  funressnfv  46958  funressnmo  46961  mosn  48544  mof02  48552  mofsn2  48558  f1omo  48574  isthinc  48688  isthincd2lem1  48694  thincmoALT  48697  thincmod  48698  isthincd  48704  setcthin  48722