Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mpt2eq123dv | Structured version Visualization version GIF version |
Description: An equality deduction for the maps to notation. (Contributed by NM, 12-Sep-2011.) |
Ref | Expression |
---|---|
mpt2eq123dv.1 | ⊢ (𝜑 → 𝐴 = 𝐷) |
mpt2eq123dv.2 | ⊢ (𝜑 → 𝐵 = 𝐸) |
mpt2eq123dv.3 | ⊢ (𝜑 → 𝐶 = 𝐹) |
Ref | Expression |
---|---|
mpt2eq123dv | ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpt2eq123dv.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐷) | |
2 | mpt2eq123dv.2 | . . 3 ⊢ (𝜑 → 𝐵 = 𝐸) | |
3 | 2 | adantr 480 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐸) |
4 | mpt2eq123dv.3 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐹) | |
5 | 4 | adantr 480 | . 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐹) |
6 | 1, 3, 5 | mpt2eq123dva 6614 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ↦ 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-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-oprab 6553 df-mpt2 6554 |
This theorem is referenced by: mpt2eq123i 6616 el2mpt2csbcl 7137 bropopvvv 7142 bropfvvvv 7144 prdsval 15938 imasval 15994 imasvscaval 16021 homffval 16173 homfeq 16177 comfffval 16181 comffval 16182 comfffval2 16184 comffval2 16185 comfeq 16189 oppcval 16196 monfval 16215 sectffval 16233 invffval 16241 isofn 16258 cofuval 16365 natfval 16429 fucval 16441 fucco 16445 coafval 16537 setcval 16550 setcco 16556 catcval 16569 catcco 16574 estrcval 16587 estrcco 16593 xpcval 16640 xpchomfval 16642 xpccofval 16645 1stfval 16654 2ndfval 16657 prfval 16662 evlfval 16680 evlf2 16681 curfval 16686 hofval 16715 hof2fval 16718 plusffval 17070 grpsubfval 17287 grpsubpropd 17343 mulgfval 17365 mulgpropd 17407 symgval 17622 lsmfval 17876 pj1fval 17930 efgtf 17958 prdsmgp 18433 dvrfval 18507 scaffval 18704 psrval 19183 ipffval 19812 phssip 19822 frlmip 19936 mamufval 20010 mvmulfval 20167 marrepfval 20185 marepvfval 20190 submafval 20204 submaval 20206 madufval 20262 minmar1fval 20271 mat2pmatfval 20347 cpm2mfval 20373 decpmatval0 20388 decpmatval 20389 pmatcollpw3lem 20407 xkoval 21200 xkopt 21268 xpstopnlem1 21422 submtmd 21718 blfvalps 21998 ishtpy 22579 isphtpy 22588 pcofval 22618 rrxip 22986 q1pval 23717 r1pval 23720 taylfval 23917 midf 25468 ismidb 25470 ttgval 25555 wlkon 26061 trlon 26070 pthon 26105 spthon 26112 is2wlkonot 26390 is2spthonot 26391 2wlkonot3v 26402 2spthonot3v 26403 grpodivfval 26772 dipfval 26941 submatres 29200 lmatval 29207 lmatcl 29210 qqhval 29346 sxval 29580 sitmval 29738 cndprobval 29822 mclsval 30714 csbfinxpg 32401 rrnval 32796 ldualset 33430 paddfval 34101 tgrpfset 35050 tgrpset 35051 erngfset 35105 erngset 35106 erngfset-rN 35113 erngset-rN 35114 dvafset 35310 dvaset 35311 dvhfset 35387 dvhset 35388 djaffvalN 35440 djafvalN 35441 djhffval 35703 djhfval 35704 hlhilset 36244 eldiophb 36338 mendval 36772 hoidmvval 39467 ovnhoi 39493 hspval 39499 hspmbllem2 39517 hoimbl 39521 mptmpt2opabbrd 40335 wwlksnon 41049 wspthsnon 41050 rngcvalALTV 41753 rngccoALTV 41780 funcrngcsetcALT 41791 ringcvalALTV 41799 ringccoALTV 41843 lincop 41991 |
Copyright terms: Public domain | W3C validator |