Theorem imbrov2fvoveq 7374

Description: Equality theorem for nested function and operation value in an implication for a binary relation. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 17-Aug-2022.)

Hypothesis

Ref	Expression
imbrov2fvoveq.1	⊢ (𝑋 = 𝑌 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
imbrov2fvoveq	⊢ (𝑋 = 𝑌 → ((𝜑 → (𝐹‘((𝐺‘𝑋) · 𝑂))𝑅𝐴) ↔ (𝜓 → (𝐹‘((𝐺‘𝑌) · 𝑂))𝑅𝐴)))

Proof of Theorem imbrov2fvoveq

Step	Hyp	Ref	Expression
1		imbrov2fvoveq.1	. 2 ⊢ (𝑋 = 𝑌 → (𝜑 ↔ 𝜓))
2		fveq2 6822	. . . 4 ⊢ (𝑋 = 𝑌 → (𝐺‘𝑋) = (𝐺‘𝑌))
3	2	fvoveq1d 7371	. . 3 ⊢ (𝑋 = 𝑌 → (𝐹‘((𝐺‘𝑋) · 𝑂)) = (𝐹‘((𝐺‘𝑌) · 𝑂)))
4	3	breq1d 5102	. 2 ⊢ (𝑋 = 𝑌 → ((𝐹‘((𝐺‘𝑋) · 𝑂))𝑅𝐴 ↔ (𝐹‘((𝐺‘𝑌) · 𝑂))𝑅𝐴))
5	1, 4	imbi12d 344	1 ⊢ (𝑋 = 𝑌 → ((𝜑 → (𝐹‘((𝐺‘𝑋) · 𝑂))𝑅𝐴) ↔ (𝜓 → (𝐹‘((𝐺‘𝑌) · 𝑂))𝑅𝐴)))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   class class class wbr 5092  ‘cfv 6482  (class class class)co 7349

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  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352

This theorem is referenced by:  rlim2  15403  rlimclim1  15452  rlimcn1  15495  climcn1  15499  caucvgrlem  15580  cncfco  24798  ftc1lem4  25944  ftc1lem6  25946  itg2gt0cn  37659  ftc1cnnclem  37675  ftc1cnnc  37676  idlimc  45611  limcperiod  45613  limclner  45636  cncfshift  45859  cncfperiod  45864  fperdvper  45904