Theorem caovclg 7619

Description: Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 26-May-2014.)

Hypothesis

Ref	Expression
caovclg.1	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥𝐹𝑦) ∈ 𝐸)

Assertion

Ref	Expression
caovclg	⊢ ((𝜑 ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) → (𝐴𝐹𝐵) ∈ 𝐸)

Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦   𝑥,𝐸,𝑦   𝜑,𝑥,𝑦   𝑥,𝐹,𝑦

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem caovclg

Step	Hyp	Ref	Expression
1		caovclg.1	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥𝐹𝑦) ∈ 𝐸)
2	1	ralrimivva 3198	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥𝐹𝑦) ∈ 𝐸)
3		oveq1 7433	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥𝐹𝑦) = (𝐴𝐹𝑦))
4	3	eleq1d 2814	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥𝐹𝑦) ∈ 𝐸 ↔ (𝐴𝐹𝑦) ∈ 𝐸))
5		oveq2 7434	. . . 4 ⊢ (𝑦 = 𝐵 → (𝐴𝐹𝑦) = (𝐴𝐹𝐵))
6	5	eleq1d 2814	. . 3 ⊢ (𝑦 = 𝐵 → ((𝐴𝐹𝑦) ∈ 𝐸 ↔ (𝐴𝐹𝐵) ∈ 𝐸))
7	4, 6	rspc2v 3622	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥𝐹𝑦) ∈ 𝐸 → (𝐴𝐹𝐵) ∈ 𝐸))
8	2, 7	mpan9 505	1 ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) → (𝐴𝐹𝐵) ∈ 𝐸)

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1533   ∈ wcel 2098  ∀wral 3058  (class class class)co 7426

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-ral 3059  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-iota 6505  df-fv 6561  df-ov 7429

This theorem is referenced by:  caovcld  7620  caovcl  7621  seqcl2  14025  seqcaopr  14044  ercpbl  17538  grpinva  18641  gsumpropd2lem  18646  imasmnd2  18738  imasgrp2  19018  gsumzaddlem  19883  imasrng  20124  imasring  20273  qusrhm  21177  qusmul2  21178  mplind  22021  plymullem  26170  qusmul  33139  fsuppssind  41857