Theorem mobidv 2550

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540  ∃*wmo 2538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-mo 2540

This theorem is referenced by:  moanimv  2620  rmobidva  3365  rmoeq1OLD  3385  mosubopt  5466  dffun6f  6515  funmo  6516  caovmo  7605  1stconst  8052  2ndconst  8053  brdom3  10450  brdom6disj  10454  imasaddfnlem  17461  imasvscafn  17470  hausflim  23937  hausflf  23953  cnextfun  24020  haustsms  24092  limcmo  25851  perfdvf  25872  rmounid  32580  rmoeqbidv  36426  disjeq12dv  36428  phpreu  37849  alrmomodm  38604  funressnfv  47397  funressnmo  47400  mosn  49166  mof02  49192  mofsn2  49198  f1omo  49246  f1omoOLD  49247  isthinc  49772  isthincd2lem1  49778  thincmoALT  49782  thincmod  49783  isthincd  49789  thincpropd  49795  indcthing  49813  discthing  49814  setcthin  49818