Theorem eqfnov2 7488

Description: Two operators with the same domain are equal iff their values at each point in the domain are equal. (Contributed by Jeff Madsen, 7-Jun-2010.)

Assertion

Ref	Expression
eqfnov2	⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐺 Fn (𝐴 × 𝐵)) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) = (𝑥𝐺𝑦)))

Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝑥,𝐹,𝑦   𝑥,𝐺,𝑦

Proof of Theorem eqfnov2

Step	Hyp	Ref	Expression
1		eqfnov 7487	. 2 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐺 Fn (𝐴 × 𝐵)) → (𝐹 = 𝐺 ↔ ((𝐴 × 𝐵) = (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) = (𝑥𝐺𝑦))))
2		simpr 484	. . 3 ⊢ (((𝐴 × 𝐵) = (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) = (𝑥𝐺𝑦)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) = (𝑥𝐺𝑦))
3		eqidd 2737	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) = (𝑥𝐺𝑦) → (𝐴 × 𝐵) = (𝐴 × 𝐵))
4	3	ancri 549	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) = (𝑥𝐺𝑦) → ((𝐴 × 𝐵) = (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) = (𝑥𝐺𝑦)))
5	2, 4	impbii 209	. 2 ⊢ (((𝐴 × 𝐵) = (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) = (𝑥𝐺𝑦)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) = (𝑥𝐺𝑦))
6	1, 5	bitrdi 287	1 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐺 Fn (𝐴 × 𝐵)) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) = (𝑥𝐺𝑦)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541  ∀wral 3051   × cxp 5622   Fn wfn 6487  (class class class)co 7358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-fv 6500  df-ov 7361

This theorem is referenced by:  fnmpoovd  8029  tpossym  8200  uncfcurf  18164  mamuass  22348  mamudi  22349  mamudir  22350  mamuvs1  22351  mamuvs2  22352  eqmat  22370  mamulid  22387  mamurid  22388  madutpos  22588  ressprdsds  24317  isngp3  24544  xrsdsre  24757  hhip  31254  1smat1  33963  matunitlindflem2  37820  eqfnovd  49132  functhinclem1  49710