Theorem mobidv 2542

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

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

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 2533

This theorem is referenced by:  moanimv  2612  rmobidva  3369  rmoeq1OLD  3389  mosubopt  5470  dffun6f  6529  funmo  6531  funmoOLD  6532  caovmo  7626  1stconst  8079  2ndconst  8080  brdom3  10481  brdom6disj  10485  imasaddfnlem  17491  imasvscafn  17500  hausflim  23868  hausflf  23884  cnextfun  23951  haustsms  24023  limcmo  25783  perfdvf  25804  rmounid  32424  rmoeqbidv  36201  disjeq12dv  36203  phpreu  37598  alrmomodm  38341  funressnfv  47044  funressnmo  47047  mosn  48801  mof02  48827  mofsn2  48833  f1omo  48881  f1omoOLD  48882  isthinc  49408  isthincd2lem1  49414  thincmoALT  49418  thincmod  49419  isthincd  49425  thincpropd  49431  indcthing  49449  discthing  49450  setcthin  49454