Theorem ovanraleqv 7434

Description: Equality theorem for a conjunction with an operation values within a restricted universal quantification. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 13-Aug-2022.)

Hypothesis

Ref	Expression
ovanraleqv.1	⊢ (𝐵 = 𝑋 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
ovanraleqv	⊢ (𝐵 = 𝑋 → (∀𝑥 ∈ 𝑉 (𝜑 ∧ (𝐴 · 𝐵) = 𝐶) ↔ ∀𝑥 ∈ 𝑉 (𝜓 ∧ (𝐴 · 𝑋) = 𝐶)))

Distinct variable groups:   𝑥,𝐵   𝑥,𝑋

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝐴(𝑥)   𝐶(𝑥)   · (𝑥)   𝑉(𝑥)

Proof of Theorem ovanraleqv

Step	Hyp	Ref	Expression
1		ovanraleqv.1	. . 3 ⊢ (𝐵 = 𝑋 → (𝜑 ↔ 𝜓))
2		oveq2 7418	. . . 4 ⊢ (𝐵 = 𝑋 → (𝐴 · 𝐵) = (𝐴 · 𝑋))
3	2	eqeq1d 2763	. . 3 ⊢ (𝐵 = 𝑋 → ((𝐴 · 𝐵) = 𝐶 ↔ (𝐴 · 𝑋) = 𝐶))
4	1, 3	anbi12d 643	. 2 ⊢ (𝐵 = 𝑋 → ((𝜑 ∧ (𝐴 · 𝐵) = 𝐶) ↔ (𝜓 ∧ (𝐴 · 𝑋) = 𝐶)))
5	4	ralbidv 3186	1 ⊢ (𝐵 = 𝑋 → (∀𝑥 ∈ 𝑉 (𝜑 ∧ (𝐴 · 𝐵) = 𝐶) ↔ ∀𝑥 ∈ 𝑉 (𝜓 ∧ (𝐴 · 𝑋) = 𝐶)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1568  ∀wral 3077  (class class class)co 7410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-ov 7413

This theorem is referenced by:  mgmidmo  18717  ismgmid  18722  ismgmid2  18725  mgmidsssn0  18729  gsumvalx  18733  gsumress  18739  sgrpidmnd  18796  ismndd  18813  mnd1  18836  gsumvallem2  18892  mhmmnd  19129  ringurd  20266  opprring  20428  pzriprnglem7  21616  pzriprnglem13  21622  zsoring  28578  signsw0g  34909  signswmnd  34910  exidu1  38451  cmpidelt  38454  exidres  38473  exidresid  38474  isrngod  38493  rngoideu  38498  zlidlring  48944  2zrngamnd  48957