Theorem mobidv 2548

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  moanimv  2618  rmobidva  3374  rmoeq1OLD  3397  mosubopt  5485  dffun6f  6549  funmo  6551  funmoOLD  6552  caovmo  7644  1stconst  8099  2ndconst  8100  brdom3  10542  brdom6disj  10546  imasaddfnlem  17542  imasvscafn  17551  hausflim  23919  hausflf  23935  cnextfun  24002  haustsms  24074  limcmo  25835  perfdvf  25856  rmounid  32476  rmoeqbidv  36231  disjeq12dv  36233  phpreu  37628  alrmomodm  38377  funressnfv  47072  funressnmo  47075  mosn  48791  mof02  48817  mofsn2  48823  f1omo  48868  isthinc  49305  isthincd2lem1  49311  thincmoALT  49315  thincmod  49316  isthincd  49322  thincpropd  49328  indcthing  49346  discthing  49347  setcthin  49351