Theorem ovmpt2ga 6688

Description: Value of an operation given by a maps-to rule. (Contributed by Mario Carneiro, 19-Dec-2013.)

Hypotheses

Ref	Expression
ovmpt2ga.1	⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆)
ovmpt2ga.2	⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)

Assertion

Ref	Expression
ovmpt2ga	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆)

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦   𝑥,𝑆,𝑦

Allowed substitution hints:   𝑅(𝑥,𝑦)   𝐹(𝑥,𝑦)   𝐻(𝑥,𝑦)

Proof of Theorem ovmpt2ga

Step	Hyp	Ref	Expression
1		elex 3185	. 2 ⊢ (𝑆 ∈ 𝐻 → 𝑆 ∈ V)
2		ovmpt2ga.2	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)
3	2	a1i 11	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅))
4		ovmpt2ga.1	. . . 4 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆)
5	4	adantl 481	. . 3 ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆)
6		simp1 1054	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → 𝐴 ∈ 𝐶)
7		simp2 1055	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → 𝐵 ∈ 𝐷)
8		simp3 1056	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → 𝑆 ∈ V)
9	3, 5, 6, 7, 8	ovmpt2d 6686	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆)
10	1, 9	syl3an3 1353	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  Vcvv 3173  (class class class)co 6549   ↦ cmpt2 6551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-iota 5768  df-fun 5806  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554

This theorem is referenced by:  ovmpt2a  6689  ovmpt2g  6693  elovmpt2  6777  offval  6802  offval3  7053  bropopvvv  7142  reps  13368  hashbcval  15544  setsvalg  15719  ressval  15754  restval  15910  sylow1lem4  17839  sylow3lem2  17866  sylow3lem3  17867  lsmvalx  17877  mvrfval  19241  opsrval  19295  marrepfval  20185  marrepval0  20186  marepvfval  20190  marepvval0  20191  cnmpt12  21280  cnmpt22  21287  qtopval  21308  flimval  21577  fclsval  21622  ucnval  21891  stdbdmetval  22129  wlkon  26061  trlon  26070  pthon  26105  spthon  26112  is2wlkonot  26390  is2spthonot  26391  2wlkonot  26392  2spthonot  26393  2wlksot  26394  2spthsot  26395  2wlkonot3v  26402  2spthonot3v  26403  resvval  29158  ofcfval3  29491  fmulcl  38648  mptmpt2opabbrd  40335